×

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].

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

Software:

Mizar; OTTER; Mathematica
PDFBibTeX XMLCite
Full Text: Link