Abstract
Knuth–Bendix completion is a classical calculus in automated deduction for transforming a set of equations into a confluent and terminating set of directed equations which can be used to decide the induced equational theory. Multi-completion with termination tools constitutes an approach that differs from the classical method in two respects: (1) external termination tools replace the reduction order—a typically critical parameter—as proposed by Wehrman et al. (2006), and (2) multi-completion as introduced by Kurihara and Kondo (1999) is used to keep track of multiple orientations in parallel while exploiting sharing to boost efficiency. In this paper we describe the inference system, give the full proof of its correctness and comment on completeness issues. Critical pair criteria and isomorphisms are presented as refinements together with all proofs. We furthermore describe the implementation of our approach in the tool \(\mathsf{mkbTT}\), present extensive experimental results and report on new completions.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Alarcón, B., Gutiérrez, R., Iborra, J., Lucas, S.: Proving termination of context-sensitive rewriting with MU-TERM. In: Proc. 6th PROLE. ENTCS, vol. 188, pp. 105–115 (2007)
Bachmair, L.: Canonical equational proofs. In: Progress in Theoretical Computer Science. Birkhäuser (1991)
Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. J. Symb. Comput. 6(1), 1–18 (1988)
Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. ACM 41(2), 236–276 (1994)
Bündgen, R., Göbel, M., Küchlin, W.: A fine-grained parallel completion procedure. In: Proc. 7th ISSAC, pp. 269–277 (1994)
Christian, J.: Fast Knuth–Bendix completion. In Proc. 3rd RTA. LNCS, vol. 355, pp. 551–555 (1989)
Dershowitz, N., Marcus, L., Tarlecki, A.: Existence, uniqueness, and construction of rewrite systems. SIAM J. Comput. 17, 629–639 (1988)
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Proc. 3rd IJCAR. LNAI, vol. 4130, pp. 281–286 (2006)
Graf, P.: Term indexing. In: LNAI, vol. 1053. Springer (1996)
Kapur, D., Musser, D.R., Narendran, P.: Only prime superpositions need be considered in the Knuth–Bendix completion procedure. J. Symb. Comput. 6(1), 19–36 (1988)
Klein, D., Hirokawa, N.: Maximal completion (system description). In: Proc. 22nd RTA. LIPIcs, vol. 10 pp. 71–80 (2011)
Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press (1970)
Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Proc. 20th RTA. LNCS, vol. 5595, pp. 295–304 (2009)
Küchlin, W.: A confluence criterion based on the generalised Newman lemma. In: Proc. 2nd EUROCAL. LNCS, vol. 204, pp. 390–399 (1985)
Kurihara, M., Kondo, H.: Completion for multiple reduction orderings. J. Autom. Reason. 23(1), 25–42 (1999)
Lescanne, P.: REVE: a rewrite rule laboratory. In: Proc. 4th International Symposium on Theoretical Aspects of Computer Science. LNCS, vol. 247, pp. 482–483 (1987)
Marché, C.: Normalized rewriting: An unified view of Knuth–Bendix completion and Gröbner bases computation. In: Symbolic Rewriting Techniques. Progress in Computer Science and Applied Logic, vol. 15, pp. 193–208. Birkhäuser (1998)
McCune, W.: Experiments with discrimination-tree indexing and path indexing for term retrieval. J. Autom. Reason. 9(2), 147–167 (1992)
Métivier, Y.: About the rewriting systems produced by the Knuth–Bendix completion algorithm. Inform. Process. Lett. 16(1), 31–34 (1983)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, pp. 371–443. Elsevier Science (2001)
Sato, H., Winkler, S., Kurihara, M., Middeldorp, A.: Multi-completion with termination tools (system description). In: Proc. 4th IJCAR. LNAI, vol. 5195, pp. 306–312 (2008)
Sato, H., Winkler, S., Kurihara, M., Middeldorp, A.: Constraint-based multi-completion procedures for term rewriting systems. IEICE Trans. Electron. E92-D(2), 220–234 (2009)
Sattler-Klein, A.: About changing the ordering during Knuth–Bendix completion. In: Proc. 11th STACS. LNCS, vol. 775, pp. 175–186 (1994)
Sekar, R., Ramakrishnan, I.V., Voronkov, A.: Term indexing. In: Handbook of Automated Reasoning, pp. 1853–1964. Elsevier Science (2001)
Steinbach, J., Kühler, U.: Check Your Ordering—Termination Proofs and Open Problems. Technical Report SR-90-25, Universität Kaiserslautern (1990)
Stump, A., Löchner, B.: Knuth–Bendix completion of theories of commuting group endomorphisms. Inform. Process. Lett. 98(5), 195–198 (2006)
Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337–362 (2009)
Voronkov, A.: The anatomy of Vampire. J. Autom. Reason. 15(2), 237–265 (1995)
Voronkov, A.: Algorithms, datastructures, and other issues in efficient automated deduction. In: Proc. 1st IJCAR. LNCS, vol. 2083, pp. 13–28 (2001)
Wehrman, I.: Knuth–Bendix completion with modern termination checking. Master’s thesis, Washington University in St. Louis, 2006. Technical report WUCSE-2006-45
Wehrman, I., Stump, A.: Mining propositional simplification proofs for small validating clauses. In: Proc. 3rd PDPAR. ENTCS, vol. 144, pp. 79–91 (2005)
Wehrman, I., Stump, A., Westbrook, E.M.: Slothrop: Knuth–Bendix completion with a modern termination checker. In: Proc. 17th RTA. LNCS, vol. 4098, pp. 287–296 (2006)
Winkler, F.: Reducing the complexity of the Knuth–Bendix completion-algorithm: a “unification” of different approaches. In: Proc. 2nd EUROCAL. LNCS, vol. 204, pp. 378–389 (1985)
Winkler, S., Middeldorp, A.: Termination tools in ordered completion. In: Proc. 5th IJCAR. LNAI, vol. 6173, pp. 518–532 (2010)
Winkler, S., Middeldorp, A.: AC completion with termination tools. In: Proc. 23rd CADE. LNAI, vol. 6803, pp. 492–498 (2011)
Winkler, S., Sato, H., Middeldorp, A., Kurihara, M.: Optimizing mkbTT (system description). In: Proc. 21st RTA. LIPIcs, vol. 6, pp. 373–384 (2010)
Author information
Authors and Affiliations
Corresponding author
Additional information
The first author is supported by a DOC-fFORTE grant of the Austrian Academy of Sciences.
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 2.0 International License (https://creativecommons.org/licenses/by/2.0), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
About this article
Cite this article
Winkler, S., Sato, H., Middeldorp, A. et al. Multi-Completion with Termination Tools. J Autom Reasoning 50, 317–354 (2013). https://doi.org/10.1007/s10817-012-9249-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-012-9249-2