Solution of the Robbins Problem

This web page is associated with a paper (with the same name) that will appear in the Journal of Automated Reasoning. Here is the preprint.

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.

The EQP proof is the same as the one in the paper.

• EQP Input
• EQP Proof

• Otter Input
• Otter Proof
• Otter Proof Object

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

The EQP proof is the same as the one in the paper.

• EQP Input
• EQP Proof

• Otter Input
• Otter Proof
• Otter Proof Object

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

(Lemma 2 is not used in the overall proof in the paper.)

• EQP Input
• EQP Proof

• Otter Input
• Otter Proof
• Otter Proof Object

Lemma 3. All Robbins algebras satisfy exists C exists D (C+D=C).

The EQP proof is the same as the one in the paper (search m5-50).

• EQP Input
• EQP Proof

• Otter Input
• Otter Proof
• Otter Proof Object

This proof is from the same search (m5-50) as the proof of Lemma 3 above.

• EQP Input (same as for Lemma 3)
• EQP Proof
• (An Otter proof hasn't been constructed.)