Prover9 Examples: Ortholattice Single Axioms

See

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

and

http://www.mcs.anl.gov/~mccune/papers/olsax/.

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.in > olsax2.out ; ### ( olsax2.out.xml )

The following job is similar to the preceding, but for OML (orthomodular lattices).

prover9 -f omlsax2.in > 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.in > mol-ss1.out ; ### ( mol-ss1.out.xml )

This one is in terms of meet, join, and complementation.

prover9 -f mol-ss2.in > mol-ss2.out ; ### ( mol-ss2.out.xml )

Prove some OML (orthomodudular lattice) properties from a nonstandard OML basis.

prover9 -f oml-4basis.in > oml-4basis.out ; ### ( oml-4basis.out.xml )

Prove some BA properties from a nonstandard BA basis.

prover9 -f ba-4basis.in > ba-4basis.out ; ### ( ba-4basis.out.xml )