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

Abstract

An automatic procedure was used to discover the fact that x ³ = 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 ³ = 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 ³ = x. This complete set of reductions can be used to decide the word problem for the x ³ = x ring.

This research was supported by the Defense Advanced Research Projects Agency under Contract N00039-80-0-0575 with the Naval Electronic Systems Command. The views and conclusions contained in this document are those of the author and should not be interpreted as representative of the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the United States government. APPROVED FOR PUBLIC RELEASE. DISTRIBUTION UNLIMITED.