×

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.

MSC:
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
PDF BibTeX XML Cite
Full Text: DOI