情報処理学会 第78回全国大会講演要旨

Lazy evaluation is a computational scheme which delays the evaluation of an expression until its value is needed, trying to improve the performance particularly when dealing with large data structure. A multi-context algebraic reasoning system is a computational system which can efficiently simulate parallel processes, each executing an algebraic reasoning procedure under a particular context (or a premise). We implemented Multi-context Completion system (lz-mkb) and Multi-context Induction system (lz-itp) with lazy evaluation mechanisms in Scala. The results show that the lazy evaluation based implementations are more efficient than the original ones.