Last October a long-standing open problem about Boolean algebras, posed by Herbert Robbins in the 1930s, was solved. It was shown that the commutativity and associativity axioms and the (so-called) Robbins equation form a basis for the variety of Boolean algebras. The result received wide-spread attention (e.g., in the New York Times), primarily because the result was established by the use of an automated theorem prover, developed by Bill McCune at Argonne National Laboratory.
We discuss the theorem proving aspects of this result, in particular the fundamental inference methods used by the theorem prover, which are based on our own work on equational reasoning.