A paper on this topic (here is the preprint) will appear in the Journal of Automated Reasoning ( JAR). The JAR paper has simpler proofs than the ones below on this page. Here are the input files and proofs corresponding to the JAR paper.
A draft of a press release, intended for a wider audience, is also available.
x + y = y + x. [commutativity] (x + y) + z = x + (y + z). [associativity] n(n(x) + y) + n(n(x) + n(y)) = x. [Huntington equation]Shortly thereafter, Herbert Robbins conjectured that the Huntington equation can be replaced with a simpler one :
n(n(x + y) + n(x + n(y))) = x. [Robbins equation]Robbins and Huntington could not find a proof, and the problem was later studied by Tarski and his students .
Algebras satisfying commutativity, associativity, and the Robbins equation became known as Robbins algebras. It is clear that every Boolean algebra is a Robbins algebra, so the interesting problem was whether every Robbins algebra is Boolean. In other words, can the Huntington equation be derived from commutativity, associativity, and the Robbins equation?
In 1979, S. Winker learned of the problem from his advisor J. Berman. L. Wos suggested that Winker attack the problem by studying Boolean conditions, such as idempotence or existence of a zero, that might make a Robbins algebra Boolean. Many such conditions were found. Several, such as each of
all x, n(n(x))=x exists 0 all x, x+0=x all x, x+x=xwere easily shown by Argonne's theorem provers to make a Robbins algebra Boolean. Winker then showed [3,4] that each of the conditions
exists C exists D, C+D=C [first Winker condition] exists C exists D, n(C+D)=n(C) [second Winker condition]also suffices, with proofs by hand using insight from theorem prover searches. In 1992 and 1996, respectively, the two Winker conditions were shown automatically to be sufficient (see the EQP preprint).
Since the early 1980s, the problem has received continued attention from mathematicians and computer scientists, but until now there has been no significant mathematical progress on the problem. (Winker's work was done in the early 1980s but not published until 1990.)
EQP proved that every Robbins algebra satisfies the second Winker condition, by refuting (with built in AC unification) the set
n(n(n(y)+x)+n(x+y)) = x. [Robbins equation] n(x+y) != n(x). [denial of 2nd Winker condition]It follows immediately from this and the Winker lemma that all Robbins algebras are Boolean.
The successful search took about 8 days on an RS/6000 processor and used about 30 megabytes of memory. (For those who have the EQP preprint, the search used basic paramodulation with the super0 restriction on AC unifiers, the pair algorithm with ratio 1, and max-weight 70.)
The input file, the proof, and EQP are available:
EQP is not yet able to construct proof objects, so the EQP proof was used to guide Otter (using AC axioms instead of AC unification) to a proof of the same theorem. Otter produced a proof object, which was then checked by the proof checker.
The input file, proof, proof object, Otter, and the proof checker are available:
Work by others on translating and checking our proofs