algebra universalis

, Volume 52, Issue 4, pp 541–549 | Cite as

Automated discovery of single axioms for ortholattices

  • W. McCune
  • R. Padmanabhan
  • M. A. Rose
  • R. Veroff
Original Paper


We present short single axioms for ortholattices, orthomodular lattices, and modular ortholattices, all in terms of the Sheffer stroke. The ortholattice axiom is the shortest possible. We also give multiequation bases in terms of the Sheffer stroke and in terms of join, meet, and complementation. Proofs are omitted but are available in an associated technical report and on the Web. We used computers extensively to find candidates, reject candidates, and search for proofs that candidates are single axioms.

Mathematics Subject Classification (2000).

03G10 06B99 

Key words and phrases.

Ortholattice basis ortholattice single identity 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Birkhäuser Verlag, Basel 2004

Authors and Affiliations

  • W. McCune
    • 1
  • R. Padmanabhan
    • 2
  • M. A. Rose
    • 3
  • R. Veroff
    • 4
  1. 1.Mathematics and Computer Science DivisionArgonne National LaboratoryArgonneUSA
  2. 2.Department of MathematicsUniversity of ManitobaWinnipegCanada
  3. 3.Department of MathematicsUniversity of Wisconsin-MadisonMadisonUSA
  4. 4.Department of Computer ScienceUniversity of New MexicoAlbuquerqueUSA

Personalised recommendations