Robbins Algebras Are Boolean

William McCune
Automated Deduction Group
Mathematics and Computer Science Division
Argonne National Laboratory
Updated March 4, 1997
These Web pages contain some information on the solution of the Robbins problem.

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.

Introduction

The Robbins problem---are all Robbins algebras Boolean?---has been solved: Every Robbins algebra is Boolean. This theorem was proved automatically by EQP, a theorem proving program developed at Argonne National Laboratory.

Historical Background

In 1933, E. V. Huntington presented [1,2] the following basis for Boolean algebra: 
    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 [5]: 
    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 [6].

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=x
were 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.)

The Solution

The proof that solves the Robbins problem was found October 10, 1996, by the theorem prover EQP. EQP is similar in many ways to our more well known program Otter. The main differences are that EQP has associative-commutative (AC) unification, is restricted to equational logic, and offers more paramodulation strategies. See the EQP preprint for details.

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:

Correctness of the Proof

Proofs found by programs are always questionable. Our approach to this problem is to have the theorem prover construct a detailed proof object and have a very simple program (written in a high-level language) check that the proof object is correct. The proof checking program is simple enough that it can be scrutinized by humans, and formal verification is probably feasible.

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:

The Winker lemmas have been checked in the same way. Look here for details.

References

  1. E. V. Huntington, ``New sets of independent postulates for the algebra of logic'', Trans. AMS 35, 274--304 (1933).
  2. E. V. Huntington, ``Boolean algebra: A correction'', Trans. AMS 35, 557--558 (1933).
  3. S. Winker, ``Robbins Algebra: Conditions That Make a Near-Boolean Algebra Boolean'', J. Automated Reasoning 6(4), 465--489 (1990).
  4. S. Winker, ``Absorption and idempotency criteria for a problem in near-Boolean algebras'', J. Algebra 153(2), 414--423 (1992).
  5. H. Robbins, phone conversation, October 15, 1996.
  6. L. Henkin, J. D. Monk, and A. Tarski, Cylindric Algebras, Part I, North-Holland, 1971.

Related Links

NY Times Story on the solution of the Robbins problem
(and some comments on the NY Times story)

Work by others on translating and checking our proofs

Two famous computer proofs