×

A complete proof of correctness of the Knuth-Bendix completion algorithm. (English) Zbl 0465.68014


MSC:

68W99 Algorithms in computer science
03B25 Decidability of theories and sets of sentences
08A99 Algebraic structures
68Q65 Abstract data types; algebraic specification
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Ballantyne, A. M.; Lankford, D. S., New Decision Algorithms for Finitely Presented Commutative Semigroups, (Report MTP-4 (May 1979), Department of Mathematics, Louisiana Tech. University) · Zbl 0449.20059
[2] Huet, G., Confluent reductions: Abstract properties and applications to term rewriting systems, J. Assoc. Comput. Mach., 27, 4, 797-821 (1980) · Zbl 0458.68007
[3] Huet, G.; Hullot, J. M., Proofs by induction in equational theories with constructors, (21st IEEE Symposium on Foundations of Computer Science, 11 (1980)), 96-107
[4] G. Huet and J. M. Hullot, Canonical form algorithms for finitely presented algebras, in preparation.; G. Huet and J. M. Hullot, Canonical form algorithms for finitely presented algebras, in preparation.
[5] Huet, G.; Oppen, D., Equations and rewrite rules: A survey, (Book, R., Formal Languages: Perspectives and Open Problems. Formal Languages: Perspectives and Open Problems, Technical Report CSL-111, SRI International, January 1980 (1980), Academic Press: Academic Press New York), Also
[6] Hullot, J. M., A Catalogue of Canonical Term Rewriting Systems, (Technical Report CSL-113 (April 1980), SRI International)
[7] Knuth, D.; Bendix, P., Simple word problems in universal algebras, (Leech, J., Computational Problems in Abstract Algebra (1970), Pergamon: Pergamon Oxford), 263-297 · Zbl 0188.04902
[8] Lankford, D. S.; Ballantyne, A. M., Decision Procedures for Simple Equational Theories With Commutative Axioms: Complete Sets of Commutative Reductions, (Report ATP-35 (March 1977), Departments of Mathematics and Computer Sciences, University of Texas at Austin) · Zbl 0449.20059
[9] Lankford, D. S.; Ballantyne, A. M.-, Decision Procedures for Simple Equational Theories With Permutative Axioms: Complete Sets of Permutative Reductions, (Report ATP-37 (April 1977), Departments of Mathematics and Computer Sciences, University of Texas at Austin) · Zbl 0449.20059
[10] 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 (Aug. 1977), Departments of Mathematics and Computer Sciences, University of Texas at Austin) · Zbl 0449.20059
[11] Peterson, G. E.; Stickel, M. E., Complete Sets of Reductions for Some Equational Theories, J. Assoc. Comput. Mach., 28, 2, 233-264 (1981) · Zbl 0479.68092
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.