Abstract
The Knuth-Bendix procedure for word problems in universal algebra is known to be very effective when it is applicable. However, the procedure will fail if it generates equations which cannot be oriented into rules (i.e., the system is not noetherian), or if it generates infinitely many rules (i.e., the system is not confluent). In 1981 Huet showed that even if the system is not confluent, the Knuth-Bendix procedure still yields a semi-decision procedure for word problems, provided that every equation can be oriented. In this paper we show that even if some equations are not orientable, the Knuth-Bendix procedure can still be modified into a reasonably efficient semi-decision procedure for word problems in equational theories. Thus, we have lifted the noetherian requirement in the Knuth-Bendix procedure. Several confluence results, extensions, and experiments are given. So are some comparisons with related work.
The proof of completeness, which is an interesting subject by itself, employs a new proof technique which utilizes a notion of transfinite semantic trees designed for proving refutational completeness of theorem proving methods in general.
The outline of the paper is as follows: Section 1 briefly introduces term rewriting. The unfailing Knuth-Bendix procedure and confluence results are given in Section 2, together with some discussions and comparisons. Section 3 extends the results to a more general theory which includes inequalities. Simplification strategies are given in Section 4. In Section 5 we present the completeness proofs, as well as a framework of theorem proving strategies which captures the deletion strategies and fairness of search plans. Section 6 describes an implementation with some experimental results. Section contains some comparisons and discussions.
Research reported in this paper is supported in part by the NSF grant DCS-8401624 and the Greco de Programmation of France.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
8. References
L. Bachmair, N. Dershowitz and J. Hsiang, Orderings for Equational Proofs, Symposium on Logic in Computer Science, Boston, June 1986.
T. Brown, “A Structured Design Method for Specialized Proof Procedures”, Ph.D. Thesis, Cal Tech., 1974.
C. L. Chang and C. T. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.
N. Dershowitz, “Orderings for Term Rewriting Systems”, J.TCS, 17, 3 (1982), 279–301.
R. Forgaard, “A Program for Generating and Analyzing Term Rewriting Systems”, Master's Thesis, MIT Lab. for Computer Science, 1984.
L. Fribourg, “SLOG: A Logic Programming Language Interpreter Based on Clausal Superposition and Rewriting”, Symposium on Logic Programming, Boston, July, 1985, 172–184.
J. Hsiang, “Two Results in Term Rewriting Theorem Proving”, Proc. of 1st International Conference in Rewrite Techniques and Applications, Dijon, May, 1985.
J. Hsiang and M. Rusinowitch, “A New Method for Establishing Refutational Completeness in Theorem Proving”, 8th CADE, Oxford, England, 1986, 141–152.
G. Huet and D. S. Lankford, “On the Uniform Halting Problem for Term Rewriting Systems”, Report 283, INRIA, 1978.
G. Huet, “A Complete Proof of Correctness of Knuth-Bendix Completion Algorithm”, J. Computer and System Sciences, 23, (1981), 11–21.
J. P. Jouannaud, P. Lescanne and F. Reinig, “Recursive Decomposition Ordering”, Conf. on Formal Description of Programming Concepts II, 1982, 331–346.
J. Jouannaud and H. Kirchner, “Completion of a Set of Rules Modulo a Set of Equations”, SIAM Journal on Computing, 15, (November 1986), 1155–1194.
D. E. Knuth and P. B. Bendix, “Simple Word Problems in Universal Algebras”, in Computational Algebra, J. Leach, (ed.), Pergamon Press, 1970, 263–297.
R. A. Kowalski and P. Hayes, “Semantic Trees in Automatic Theorem Proving”, in Machine Intelligence, vol. 5, B. Meltzer and D. Michie, (eds.), American Elsevier, 1969, 181–201.
R. Kowalski, “Search Strategies for Theorem Proving”, in Machine Intelligence, vol. 5, B. Meltzer and D. Michie, (eds.), American Elsevier, 1970, 181–201.
D. S. Lankford, “Canonical Inference”, Report ATP-32, Univ. of Texas at Austin, 1975.
D. S. Lankford and A. M. Ballantyne, “Decision Procedure for Simple Equational Theories with Commutative-Associative Axioms”, Report ATP-39, Univ. of TExas at Austin, 1977.
J. Mzali, “Methodes de Filtrage Equationnel et de Preuve Automatique de Theoremes”, These de Doctorat de l'Universite de Nancy I, 1986.
J. Pedersen, “Obtaining Complete Sets of Reductions and Equations without using Special Unification Algorithms”, Unpublished manuscript, 1985.
G. E. Peterson and M. E. Stickel, “Complete Sets of Reductions for Some Equational Theories”, J. ACM, 28, (1981), 233–264.
G. E. Peterson, “A Technique for Establishing Completeness Results in Theorem Proving with Equality”, SIAM J. of Computing, 12, 1 (1983), 82–100.
D. A. Plaisted, “A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems”, UIUCDCS-R-78-943, Univ. of Illinois, Urbana, IL, 1978.
D. Plaisted, “Private Communication”,, 1985.
K. Sakai, “Knuth-Bendix Algorithm for Thue System Based on Kachinuki Ordering”, Technical Report, 0087, ICOT, 1985.
“Assoc. of Automated Reasoning Newsletter”,, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hsiang, J., Rusinowitch, M. (1987). On word problems in equational theories. In: Ottmann, T. (eds) Automata, Languages and Programming. ICALP 1987. Lecture Notes in Computer Science, vol 267. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-18088-5_6
Download citation
DOI: https://doi.org/10.1007/3-540-18088-5_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-18088-3
Online ISBN: 978-3-540-47747-1
eBook Packages: Springer Book Archive