Advertisement

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

  • Mark E. Stickel
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

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.MathSciNetzbMATHGoogle Scholar
  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.CrossRefGoogle Scholar
  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

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Mark E. Stickel
    • 1
  1. 1.Artificial Intelligence CenterSRI InternationalMenlo Park

Personalised recommendations