Implementation and performance evaluation of multi-completion with termination checking

In equational theorem proving, convergent term rewriting systems play a crucial role. In order to compute convergent term rewriting systems, the standard completion procedure (KB) was proposed by Knuth and Bendix and has been improved in a various way. The multi-completion system MKB developed by Kurihara and Kondo accepts as input a set of reduction orders in addition to equations and efficiently simulates parallel processes each of which executes the KB procedure with one of the given orderings. Wehrman and Stump also developed a new variant of completion procedure, constraint-based completion, in which reduction orders need not be given by using automated modern termination checker. As a result, the constraint-based procedures simulate the execution of parallel KB processes in a sequential way, but the naive breadth-first search sometimes causes serious inefficiency when the number of the potential reduction orders is large. We present a new procedure, called a constraint-based multi-completion procedure MKBcs, by augmenting the constraint-based completion with the framework of the multi-completion suppressing the combinatorial explosion by sharing inferences among the processes.