Parallelization of Termination Checker of Term Rewriting Systems.

Inductive theorem proving plays an important role in the field of formal verification of systems. The rewriting induction(RI) is a method for inductive theorem proving proposed by Reddy. And the multi-context rewriting induction(MRI) proposed by Sato based on the idea of Kurihara has improved the power of RI significantly. However a large amount of termination check of term rewriting systems should be performed in the MRIt, which is becoming the efficiency bottleneck of MRI. In this paper, we propose a method of parallelizing the termination checker used in MRI based on the lexicographic path order method to improve its efficiency. And then we will discuss its efficiency based on the experiments with the system implemented in a parallel functional programming language named Erlang. [ABSTRACT FROM AUTHOR]