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.