# A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that x3 = x Implies Ring Commutativity

• Mark E. Stickel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)

## Abstract

An automatic procedure was used to discover the fact that x 3 = x implies ring commutativity. The proof of this theorem was posed as a challenge problem by W.W. Bledsoe in a 1977 article. The only previous atttomated proof was by Robert Veroff using the Argonne National Laboratory — Northern Illinois University theorem-proving system. The technique used to prove this theorem was the Knuth-Bendix completion method with associative and/or commutative unification. This was applied to a set of reductions consisting of a complete set of reductions for free rings plus the reduction x × x × x → and resulted in the purely forward-reasoning derivation of x × y = y × x. An important extension to this methodology, which made solution of the x 3 = x ring problem feasible, is the use of cancellation laws to simplify derived reductions. Their use in the Knuth-Bendix method can substantially accelerate convergence of complete sets of reductions. A second application of the Knuth-Bendix method to the set of reductions for free rings plus the reduction x × x × x → x, but this time with the commutativity of multiplication assumed, resulted in the discovery of a complete set of reductions for free rings satisfying x 3 = x. This complete set of reductions can be used to decide the word problem for the x 3 = x ring.

## References

1. [1]
Bledsoe, W.W. Non-resolution theorem proving. Artificial Intelligence 9,1 (August 1977), 135.Google Scholar
2. [2]
Comer, S.D. Elementary properties of structures of sections. Boletin de la Sociedad Matematica Mexicana 19 (1974), 78–85.
3. [3]
Huet, G. A complete proof of the correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Sciences 23,1 (August 1981), 11–21.Google Scholar
4. [4]
Huet, G. and J.M. Hullot. Proofs by induction in equational theories with constructors. Proceedings of the 21st IEEE Symposium on the Foundations of Computer Science, 1980.Google Scholar
5. [5]
Hullot, J.M. A catalogue of canonical term rewriting systems. Technical Report CSL-113, Computer Science Laboratory, SRI International, Menlo Park, California, April 1980.Google Scholar
6. [6]
Jacobson, N. Structure theory for algebraic algebras of bounded degree. Annals of Mathematics 46,4 (October 1945), 695–707.Google Scholar
7. [7]
Knuth, D.E. and P.B. Bendix. Simple word problems in universal algebras. In Leech, J. (ed.), Computational Problems in Abstract Algebras, Pergamon Press, 1970, pp. 263–297.Google Scholar
8. [8]
Lankford, D.S. Canonical algebraic simplification. Report ATP-25, Department of Mathematics, University of Texas, Austin, Texas, May 1975.Google Scholar
9. [9]
Lankford, D.S. Canonical inference. Report ATP-32, Department of Mathematics, University of Texas, Austin, Texas, December 1975.Google Scholar
10. [10]
Lankford, D.S. and A.M. Ballantyne. Decision procedures for simple equational theories with commutative axioms: complete sets of commutative reductions. Report ATP-35, Department of Mathematics, University of Texas, Austin, Texas, March 1977.Google Scholar
11. [11]
Lankford, D.S. and A.M. Ballantyne. Decision procedures for simple equational theories with permutativc axioms: complete sets of permutative reductions. Report ATP-37, Department of Mathematics, University of Texas, Austin, Texas, April 1977.Google Scholar
12. [12]
Lankford, D.S. and A.M. Ballantyne. Decision procedures for simple equational theories with commutative-associative axioms: complete sets of commutative-associative reductions. Report ATP-39, Department of Mathematics, University of Tcxes, Austin, Texas, August 1977.Google Scholar
13. [13]
Livesey, M. and J. Siekmann. Termination and decidability results for string-unification. Memo CSM-12, Essex University Computing Center, Colchester, Essex, England, August 1975.Google Scholar
14. [14]
Livesey, M. and J. Siekmann. Unification of A+C-terms (bags) and A+C+I-terms (sets). Interner Bericht Nr. 5/76, Institut für Informatik I, Universität Karlsruhe, Karlsruhe, West Germany, 1976.Google Scholar
15. [15]
Peterson, G.E. and M.E. Stickel. Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery 28,2 (April 1981), 233–264.Google Scholar
16. [161.
Peterson, G.E. and M.E. Stickel. Complete systems of reductions using associative and/or commutative unification. Technical Note 269, Artificial Intelligence Center, SRI International, Menlo Park, California, October 1982. To appear in M. Richter (ed.) Lecture Notes on Systems of Reductions.Google Scholar
17. [17]
Siekmanu, J. String-unification, part I. Essex University, Cochestcr, Essex, England, March 1975.Google Scholar
18. [18]
Siekmann, J. T-unification, part I. Unification of commutative terms. Interner Bericht Nr. 4/76, Institut für Informatik I, Universität Karlsruhe, Karlsruhe, West Germany, 1976.Google Scholar
19. [19]
Sticke], M.E. Mechanical theorem proving and artificial intelligence languages. Ph.D. Dissertation, Department of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania., December 1977.Google Scholar
20. [20]
Stickel, M.E. A unification algorithm for associative-commutative functions. Journal of the Association for Computing Machinery 28,3 (July 1981), 423–434.Google Scholar
21. [211.
Veroff, R.L. Canonicalization and demodulation. Report ANL-81-6, Argonne National Laboratory, Argonne, Illinois, February 1981.
22. [22]
Winkler, F. A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. CAMP-LINZ Technical Report 83-14.0, Ordinariat Mathematik III, Johannes Kepler Universität, Linz, Austria, May 1983.Google Scholar