Abstract

In this paper we describe a new tool for performing Knuth-Bendix
completion with automatic termination tools. It is based on two
ingredients: (1) the inference system for completion with multiple
reduction orderings introduced by Kurihara and Kondo (1999) and
(2) the inference system for completion with external termination
provers proposed by Wehrman, Stump and Westbrook (2006) and
implemented in the Slothrop system. Our tool can be used with
any termination tool that satisfies certain minimal requirements.
Preliminary experimental results show the potential of our tool.

BibTeX

@inproceedings{HSSWMKAM-IJCAR08,
  author      = "Haruhiko Sato and Sarah Winkler and Masahito Kurihara and
                 Aart Middeldorp",
  title       = "Multi-Completion with Termination Tools (System
                 Description)",
  booktitle   = "Proceedings of the 4th International Joint Conference on
                 Automated Reasoning",
  series      = "Lecture Notes in Artificial Intelligence",
  volume      = "5195",
  pages       = "306--312",
  publisher   = "Springer-Verlag",
  year        = 2008
}