These web pages are a supplement to the following paper.

Automatic Proofs and Counterexamples
for Some Ortholattice Identities

W. McCune

The paper has appeared in Information Processing Letters 65 (1998) 285--291. Here is a preprint.


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.