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 )