Posted on the Web June 21, 2002. Last updated on June 21, 2002 by Bob Veroff.

Robbins Algebra

In October 1996, Bill McCune used an automated reasoning program to prove that all Robbins algebras are Boolean. This problem had intrigued researchers for several years, and its solution received quite a bit of attention. Bill maintains a Web site here that includes discussion, input and output files, and references.

Bill's proof was based on proving a condition (actually, a sequence of conditions) that had previously been shown to suffice. One of the earliest known sufficient conditions was to derive an equation known has Huntington's axiom. See Bill's Web site for a full discussion.

To the best of our knowledge, presentations of the proof that Robbins algebras are Boolean have remained in the form of sequences of proofs, eventually leading to a proof of Huntington's equation. Here is a single Otter derivation of Huntington's axiom. Here is an Otter input file that can be used to check the derivation.

The University of New Mexico

School of Engineering

Computer Science Department