Prover9 Examples: Ortholattice Single Axioms

McCune, Padmanabhan, Rose, Veroff, "Automated Discovery of Single Axioms for Ortholattices", Algebra Universalis 52, pp. 541-549 (2005).

Starting with a single axiom for OL (ortholattices) in terms of the Sheffer stroke, prove an OL 3-basis, which is also in terms of the Sheffer stroke. This job introduces the meet, join, and complememtation operations to help the search.
prover9 -f > olsax2.out ; ### ( olsax2.out.xml )
The following job is similar to the preceding, but for OML (orthomodular lattices).
prover9 -f > omlsax2.out ; ### ( omlsax2.out.xml )
The following two jobs show that two MOL (modular ortholattice) bases are definitionally equivalent. This one is in terms of the Sheffer stroke.
prover9 -f > mol-ss1.out ; ### ( mol-ss1.out.xml )
This one is in terms of meet, join, and complementation.
prover9 -f > mol-ss2.out ; ### ( mol-ss2.out.xml )
Prove some OML (orthomodudular lattice) properties from a nonstandard OML basis.
prover9 -f > oml-4basis.out ; ### ( oml-4basis.out.xml )
Prove some BA properties from a nonstandard BA basis.
prover9 -f > ba-4basis.out ; ### ( ba-4basis.out.xml )