×

Only prime superpositions need be considered in the Knuth-Bendix completion procedure. (English) Zbl 0651.68029

The Knuth and Bendix test for local confluence of a term rewriting system involves generating superpositions of the left-hand sides, and for each superposition deriving a critical pair of terms and checking whether these terms reduce to the same term. We prove that certain superpositions, which are called composite because they can be split into other superpositions, do not have to be subjected to the critical-pair- joinability test; it suffices to consider only prime superpositions. As a corollary, this result settles a conjecture of Lankford that unblocked superpositions can be omitted.
To prove the result, we introduce new concepts and proof techniques which appear useful for other proofs relating to the Church-Rosser property. This test has been implemented in the completion procedures for ordinary term rewriting systems as well as term rewriting systems with associative-commutative operators. Performance of the completion procedures with this test and without the test are compared on a number of examples in the Rewrite Rule Laboratory (RRL) being developed at General Electric Research and Development Center.

MSC:

68Q65 Abstract data types; algebraic specification
68W30 Symbolic computation and algebraic computation
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

REVE; RRL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bachmair, L.; Dershowitz, N., Critical pair criteria for the Knuth-Bendix completion procedure (1986), University of Illinois at Urbana Champaign, Extended abstract appeared in the Proc. of SYMSAC’86
[2] Bledsoe, W. W., Non-resolution theorem proving, Artificial Intelligence, 9, 1-35 (1977) · Zbl 0358.68131
[3] Buchberger, B., A criterion for detecting unnecessary reductions in the construction of Gröbner Bases, (Proceedings of EUROSAM 79 (1979), Springer Verlag), 3-21, Lecture Notes in Computer Science 72 · Zbl 0417.68029
[4] Dershowitz, N.; Manna, Z., Proving termination with multiset orderings, Comm. ACM, 22/8, 465-476 (1979) · Zbl 0431.68016
[5] Fages, F., Associative-commutative unification, (Proc. of 7th International Conference on Automated Deduction (1984), Springer Verlag), 3-21, Lecture Notes in Computer Science 170 · Zbl 0547.03012
[6] Fortenbacher, A., An algebraic approach to unification under associativity and commutativity, (Proc. of First International Conference on Rewriting Techniques and Applications (1985), Springer Verlag), Lecture Notes in Computer Science · Zbl 0581.68029
[7] (Guttag, J. V.; Kapur, D.; Musser, D. R., Proceedings of an NSF Workshop on the Rewrite Rule Laboratory. Proceedings of an NSF Workshop on the Rewrite Rule Laboratory, Sept. 6-9 Sept. 1983 (1984)), General Electric Research and Development Center Report 84GEN008
[8] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, J ACM, 27/4, 797-821 (1980) · Zbl 0458.68007
[9] Huet, G.; Hullot, J. M., Proofs by induction in equational theories with constructors, (21st IEEE Symposium on Foundations of Computer Science (1980)), 96-107
[10] Hullot, J. M., A catalogue of canonical term rewriting systems, (Technical Report CSL-13, Computer Science Laboratory (1980), SRI International: SRI International Menlo Park)
[11] Jouannaud, J.; Kirchner, H., Completion of a set of rules modulo a set of equations, (Proc. of Principles of Programming Languages (POPL) (1984)) · Zbl 0665.03005
[12] Jouannaud, J.; Kounalis, E., Automatic proofs by induction in equational theories without constructors, (Proc. of Symposium on Logic in Computer Science (1986)), 358-366
[13] Kapur, D.; Musser, D. R., Proof by consistency, Artificial Intelligence, 31, 125-157 (1987) · Zbl 0631.68073
[14] Kapur, D.; Narendran, P.; Zhang, H., Proof by induction using test sets, (8th Intl. Conf. on Automated Deduction (1986), Springer Verlag), Lecture Notes in Computer Science · Zbl 0642.68034
[15] Kapur, D.; Sivakumar, G., Architecture of and experiments with RRL, a Rewrite Rule Laboratory, Comm. ACM, 4, 33-56 (1984), In: Reference
[16] Kapur, D.; Sivakumar, G.; Zhang, H., RRL: A Rewrite Rule Laboratory, (8th Intl. Conf. on Automated Deduction (1986), Springer Verlag), Lecture Notes in Computer Science
[17] Knuth, D. E.; Bendix, P. B., Simple word problems in universal algebras, (Leech, J., Computational Problems in Abstract Algebras (1970), Pergamon Press), 263-297 · Zbl 0188.04902
[18] Küchlin, W., A confluence criterion based on the generalized Newman Lemma, (Caviness, EURO-CAL ’85, 2 (1985), Springer Verlag), 390-399, Lecture Notes in Computer Science, 204
[19] Lankford, D. S., Canonical inference, Univ. of Texas, Math. Dept. Automatic Theorem Proving Project, Austin, Texas, Report ATP-32 (1975)
[20] Lankford, D. S.; Ballantyne, A. M., Decision procedures for simple equational theories with commutative-associative axioms: complete sets of commutative-associative reductions, Report ATP-39 (1977), Dept. of Math, and Computer Science, University of Texas: Dept. of Math, and Computer Science, University of Texas Austin, Texas
[21] Lankford, D. S.; Ballantyne, A. M., The refutation completeness of blocked permutative narrowing and resolution, (Proc. of Fourth Workshop on Automated Deduction. Proc. of Fourth Workshop on Automated Deduction, Austin, Texas (1979))
[22] Lescanne, P., Computer experiments with the REVE term rewriting system generator, Proc. of 10th Principles of Programming Languages (POPL) (1983), Conference
[23] Musser, D. R., On proving inductive properties of abstract data types, Proc. 7th Principles of Programming Languages (POPL) (1980)
[24] Musser, D. R., Abstract data types in the AFFIRM system, IEEE Trans, on Software Engineering, SE-6/1 (1980) · Zbl 0431.68022
[25] Musser, D. R.; Kapur, D., Rewrite rule theory and abstract data type analysis, (Calmet, Computer Algebra, EUROCAM, 1982 (1982), Springer Verlag), 77-90, Lecture Notes in Computer Science 144
[26] Peterson, G. L.; Stickel, M. E., Complete sets of reductions for some equational theories, J ACM, 28/2, 233-264 (1981) · Zbl 0479.68092
[27] Slagle, J., Automated theorem proving for theories with simplifiers, commutativity and associativity, J. ACM, 4, 622-642 (1974) · Zbl 0296.68092
[28] Stickel, M. E., A unification algorithm for associative-commutative functions, Journal of the ACM, 28, 3, 423-434 (1981) · Zbl 0462.68075
[29] Winkler, F.; Buchberger, B., A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm, (Proc. of the Coll. on Algebra, Combinatorics and Logic in Computer Science (1983)) · Zbl 0607.03003
[30] Winkler, F., The Church-Rosser property in computer algebra and special theorem proving: an investigation of critical pair, completion algorithms, (Dissertation der J. Kepler-Universitaet, Linz, Austria (1984)) · Zbl 0562.68023
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.