# A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that *x*^{3} = *x* Implies Ring Commutativity

## 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.

## Preview

Unable to display preview. Download preview PDF.

## References

- [1]Bledsoe, W.W. Non-resolution theorem proving.
*Artificial Intelligence 9*,1 (August 1977), 135.Google Scholar - [2]Comer, S.D. Elementary properties of structures of sections.
*Boletin de la Sociedad Matematica Mexicana 19*(1974), 78–85.MathSciNetzbMATHGoogle Scholar - [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]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]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]Jacobson, N. Structure theory for algebraic algebras of bounded degree.
*Annals of Mathematics 46*,4 (October 1945), 695–707.Google Scholar - [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]Lankford, D.S. Canonical algebraic simplification. Report ATP-25, Department of Mathematics, University of Texas, Austin, Texas, May 1975.Google Scholar
- [9]Lankford, D.S. Canonical inference. Report ATP-32, Department of Mathematics, University of Texas, Austin, Texas, December 1975.Google Scholar
- [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]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]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]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]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]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 - [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]Siekmanu, J. String-unification, part I. Essex University, Cochestcr, Essex, England, March 1975.Google Scholar
- [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]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]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 - [211.Veroff, R.L. Canonicalization and demodulation. Report ANL-81-6, Argonne National Laboratory, Argonne, Illinois, February 1981.CrossRefGoogle Scholar
- [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