Grabowski, Adam Robbins algebras vs. Boolean algebras. (English) Zbl 0984.06500 Buchberger, Bruno (ed.) et al., Mathematical knowledge management: MKM 2001. Electronic proceedings of the 1st international workshop, RISC, Schloß Hagenberg, Austria, September 24-26, 2001. Linz: Univ. Linz, 12 p. (2001). Summary: In the early 1930s, Huntington proposed several axiom systems for Boolean algebras. Robbins slightly changed one of them and asked if the resulted system is still a basis for the variety of Boolean algebras. A partial solution has been given by Winker in 1992, and in 1996 McCune with the help of a theorem prover gave the positive answer. Some simplified and restructurized versions of this proof are known. We describe in this paper some of the issues concerned with a fully mechanically checked proof of the fact that all Robbins algebras are Boolean.For the entire collection see [Zbl 0978.00042]. Cited in 2 ReviewsCited in 4 Documents 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 Keywords:machine-supported proof; Boolean algebras; Robbins algebras Software:Mizar; OTTER; Mathematica PDFBibTeX XMLCite \textit{A. Grabowski}, in: Mathematical knowledge management: MKM 2001. Electronic proceedings of the 1st international workshop, RISC, Schloß Hagenberg, Austria, September 24--26, 2001. Linz: Univ. Linz. 12 p. (2001; Zbl 0984.06500) Full Text: Link