Prover9 Examples: Uniquely Complemented Lattices

These theorems are on Huntington equations, that is, equations that force uniquely complemented lattices to be Boolean. Examples are distributivity and modularity.

This work is part of a project of Padmanabhan, Veroff, and McCune.


The following job shows that lattice identity H27 is a Huntington identitiy by proving distributivity in uniquely complemented lattices.
prover9 -f lt.in uc.in H27d.in > H27d.out ; ### ( H27d.out.xml )
Same for H65.
prover9 -f lt.in uc.in H65d.in > H65d.out ; ### ( H65d.out.xml )
The following four jobs show that lattice identities H42, H49, H78, and H7 are Huntington identities by proving a ≤ b -> b' ≤ a in uniquely complemented lattices.

H42 is Huntington.

prover9 -f lt.in uc.in H42.in > H42.out ; ### ( H42.out.xml )
H49 is Huntington.
prover9 -f lt.in uc.in H49.in > H49.out ; ### ( H49.out.xml )
H78 is Huntington.
prover9 -f lt.in uc.in H78b.in > H78b.out ; ### ( H78b.out.xml )
H7 is Huntington.
prover9 -f lt.in uc.in H7b.in > H7b.out ; ### ( H7b.out.xml )
Huntington identity H33 imples Huntington H34 in ordinary lattice theory (without complementation).
prover9 -f lt.in H33-H34.in > H33-H34.out ; ### ( H33-H34.out.xml )
Same for H39 implies H3.
prover9 -f lt.in H39-H3.in > H39-H3.out ; ### ( H39-H3.out.xml )