Abstract

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 various ways. 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 checkers. As a result,
the constraint-based procedures simulate the execution of parallel KB
processes in a sequential way, but naive search algorithms sometimes
cause serious inefficiency when the number of the potential reduction
orders is large. In this paper, 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
for suppressing the combinatorial explosion by sharing inferences among
the processes. The existing constraint-based system Slothrop, which
basically employs the best-first search, is more efficient when its
built-in heuristics for process selection are appropriate, but when they
are not, our system is more efficient. Therefore, both systems have their
role to play.

BibTeX

@article{HSMKSWAM-IEICE09,
  author      = "Haruhiko Sato and Masahito Kurihara and Sarah Winkler and
                 Aart Middeldorp",
  title       = "Constraint-Based Multi-Completion Procedures for Term
                 Rewriting Systems",
  journal     = "IEICE Transactions on Information and Systems",
  volume      = "E92-D",
  number      = 2,
  pages       = "220--234",
  year        = 2009
}