These web pages are a supplement to the following paper.
Automatic Proofs and Counterexamples
for Some Ortholattice Identities
The paper has appeared in Information Processing Letters
65 (1998) 285--291.
Here is a
preprint.
Abstract
The paper answers questions on
whether three identities known to hold
for orthomodular lattices are true also for ortholattices.
One is shown to fail by
MACE,
a program that searches for
counterexamples, an the other two are proved to hold by
EQP,
an equational theorem prover.
The problems, from work in quantum logic,
were given to us by Norman Megill and Mladen Pavicic.
Files Available
Counterexample for equation E1:
MACE input, MACE output.
Proof for equation E2:
EQP input, EQP proof.
Proof for equation E3:
EQP input, EQP proof.
Counterexample for equation E4:
MACE input, MACE output.
Verification that the E1 ortholattice violates E4:
MACE input, MACE output.