Robbins algebra
From Wikipedia, the free encyclopedia
A Robbins algebra is an algebra consisting of the set {0,1} and the logical operations 
(disjunction, "or") and 
(negation, "not"), with the following axioms:
- Associativity:
- Commutativity:
- Robbins' axiom:
The Robbins conjecture, posed by Herbert Robbins, is that these axioms are equivalent to those of Boolean algebras. The conjecture was proven in 1996 by William McCune, using an automated theorem prover.
[edit] History
In 1933, Edward Huntington proposed an alternative set of axioms for Boolean algebras, consisting of the aforementioned axioms of associativity and commutativity plus Huntington's axiom:
The validity of this axiom in Boolean logic can easily be proved using its truth table. Huntington also showed the three axioms together imply the axioms of Boolean algebra.
Some time after, Robbins conjectured that his (simpler) axiom implies that of Huntington, so that Robbins algebras are equivalent with Boolean algebras. Huntington, Robbins and Alfred Tarski worked on the problem, but failed to find a proof or counterexample. The proof was finally delivered in 1996 by William McCune, using his theorem prover EQP.
[edit] External links
- Computer Math Proof Shows Reasoning Power, New York Times, December 10, 1996.
- Edward Nelson, Automated Reasoning (course notes)
