Robbins Algebra Lemmas


Draft -- October 24, 1996
This page contains the three Robbins algebra lemmas that are used in the solution of the Robbins problem. Lemma 1 uses Lemma 0, Lemma 2 uses Lemma 1, and the solution of the Robbins problem uses Lemma 2. Very orderly. These lemmas were first proved by Steve Winker in the early 1980s.

The EQP proofs use associative-commutative unification, and the Otter proofs use associativity and commutativity as axioms.

Lemma 0. Robbins algebras satisfying exists C, C+C=C are Boolean.

Lemma 1. Robbins algebras satisfying exists C exists D, C+D=C are Boolean.

Lemma 2. Robbins algebras satisfying exists C exists D, n(C+D)=n(C) are Boolean.


You can use Otter to prove some of the easier Robbins lemmas right now with Son of BirdBrain.
William McCune,
Automated Deduction Group,
Mathematics and Computer Science Division,
Argonne National Laboratory