Short equational bases for ortholattices : proofs and countermodels.
WILLIAM S. MCCUNE, Ranganathan Padmanabhan, M A Rose, Robert Veroff · 2004
This document contains proofs and countermodels in support of the paper ''Short Equational Bases for Ortholattices'', by the same set of authors. In that paper, 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. Computers were used extensively to find candidates, reject candidates, and search for proofs that candidates are single axioms.