Publications

W. McCune, R. Padmanabhan, M. A. Rose, R. Veroff, "Short Equational Bases for Ortholattices," Preprint ANL/MCS-P1087-0903, September 2003. [pdf]

Short single axioms for ortholattices, orthomodular lattices, and modular ortholattices are presented, all in terms of the Sheffer stroke. The ortholattice axiom is the shortest possible.
Other equational bases in terms of the Sheffer stroke and in terms of join, meet, and complement are presented. Proofs are omitted but are available in an associated technical report. Computers were used extensively to find candidates, reject candidates, and search for proofs that candidates are single axioms. The notion of computer proof is addressed.