zbMATH — the first resource for mathematics

Solution of the Robbins problem. (English) Zbl 0883.06011
Summary: We show that the three equations known as commutativity, associativity, and the Robbins equation are a basis for the variety of Boolean algebras. The problem was posed by Herbert Robbins in the 1930s. The proof was found automatically by EQP, a theorem-proving program for equational logic. We present the proof and the search strategies that enabled the program to find the proof.

06E05 Structure theory of Boolean algebras
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
06-04 Software, source code, etc. for problems pertaining to ordered structures
Full Text: DOI