@MISC{ROBBINS1.MIZ,
  AUTHOR = {Grabowski, Adam},
  TITLE = {Robbins Algebras vs. {B}oolean Algebras},
  NOTE = {This work has been partially supported by TYPES grant IST-1999-29001.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Pre-Ortholattices},
  SECTION3 = {Correspondence between Boolean Pre-OrthoLattices and Boolean Lattices},
  SECTION4 = {Proofs according to Bernd Ingo Dahn},
  SECTION5 = {Proofs according to William McCune},
  DAY = {12},
  MONTH = {June},
  YEAR = {2001},
  ADDRESS1 = {University of Bia{\l}ystok},
  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 variety of Boolean algebras. The solution
 (afirmative answer) was given in 1996 by McCune with
 the help of automated theorem prover EQP/{\sc Otter}.
 Some simplified and restucturized versions of this proof
 are known.
 In our version of proof that all Robbins algebras
 are Boolean we use the results of McCune \cite{McCuneRob},
 Huntington \cite{Huntington1}, \cite{Huntington2}, \cite{Huntington3}
 and Dahn \cite{DahnRob}.}}

