Parallelization of termination checker for term rewriting system

摘要

An inductive theorem is an equation over terms which holds on recursively-defined data structure. In the field of formal verification of information system, inductive theorem proving plays an important role. Rewriting induction(RI) is a method for inductive theorem proving proposed by Reddy. Multi-context rewriting induction with termination checker (MRIt) proposed by Sato is a variant of RI which tries to find a suitable context for induction automatically. However, MRIt should perform a large amount of termination checking of term rewriting systems which is becoming efficiency bottleneck. In this paper, we propose a method of parallelizing the termination checker used in MRIt based on the lexicographic path order method to improve its efficiency. For implementation, we used the functional programming language Erlang. We discuss the efficiency of our implementation based on the experiments.