A New Implementation Of Multi-context Algebraic Inductive Theorem Prover

摘要/ABSTRACT

Term rewriting induction (RI) is a principle for automatic inductive theorem proving proposed by Reddy. There are several strategic issues in RI: (1) which reduction order should be applied, (2) which (axiomatic or hypothetical) rules should be applied during rewriting, and (3) which variables should be instantiated for induction. The multi-context rewriting induction with termination checker (MRIt) solved these problems by creating virtual parallel processes dynamically to handle the nondeterministic choices. In this paper, we present a multi-context algebraic inductive theorem prover called lz-itp and implement it in a functional, object-oriented programming language Scala which features the lazy evaluation mechanism. Based on MRIt, our implementation exploits the lazy evaluation schemas to gain efficiency. Also the automatic lemma generations are employed to support solving the lemmarequired
problems. The experiments show that lz-itp is more efficient than the original MRIt implementation of Sato and Kurihara.

作者/Authors

ChengCheng Ji, Masahito Kurihara, Haruhiko Sato

会议信息/Information

Lecture Notes in Engineering and Computer Science: Proc. The World Congress on Engineering and Computer Science 2015, San Francisco, USA, pp. 109-114 (EI).

季承成 | CHENGCHENG JI