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