Robbins Algebras Are Boolean: A Revision of McCuneʹs Computer-Generated Solution of Robbins Problem

In the early 1930s, Robbins asked whether a certain equation together with commutativity and associativity of the union operation was sufficient to characterize Boolean algebras. In 1992, Winker reduced this to the problem of proving the solvability of another equation from Robbinsʹ axioms. In October 1996, William McCune confirmed Winkerʹs condition with the help of the automated theorem prover EQP. In this paper we give a simplified presentation of the proof discovered by EQP.