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. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Sato, H., Winkler, S., Kurihara, M., & Middeldorp, A. (2008). Multi-completion with termination tools (system description). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5195 LNAI, pp. 306–312). https://doi.org/10.1007/978-3-540-71070-7_26
Mendeley helps you to discover research relevant for your work.