Short Equational Bases for Ortholattices: Web Support
William McCune,
R. Padmanabhan,
Michael A. Rose,
Robert Veroff
There are several parts to the documentation of the project.
 A short paper for a journal.
 Version v16:
PDF,
tex
(Sept 10, 2004),
minor revision from v15, as suggested by referee.
 Version v15 (Feb 23, 2004),
submitted for publication.
 A paper for a wide audience.
 Version v10 (Oct 30, 2003);
The American Mathematical Monthly declined to publish this.
 A set of Web pages (this page is the root) containing proofs,
countermodels, and additional background and explanation.
These are for immediate support of the papers.
 A technical report containing proofs and countermodels.
This is for archival support of the papers.
Son of BirdBrain, the
Webbased demo of Otter and Mace2, can prove most of the easy theorems
and find most of the countermodels cited in the papers.
Try it now 
select the area "Ortholattices".
Abstract (from the v10 paper)
Short single axioms for ortholattices, orthomodular lattices, and
modular ortholattices are presented, all in terms of the Sheffer
stroke. The ortholattice axiom is the shortest possible.
Other equational bases in terms of the Sheffer stroke and
in terms of join, meet, and complement are presented.
Proofs are
omitted but are available in an associated technical report.
Computers were used extensively to find candidates, reject candidates,
and search for proofs that candidates are single axioms. The notion
of computer proof is addressed.
1 Introduction
The structure of this page roughly follows the v10 paper, with similar
section titles.
The following notes give some explanation of the proofs and countermodels.
2 Equational Bases
2.1 In Terms of Join/Meet/Complement
These links lead to the join/meet/complement bases for the varieties,
including proofs of various properties and independence proofs cited
in the papers.
2.2 In Terms of the Sheffer Stroke
These links lead to the Sheffer stroke bases for the varieties.
Proofs that the bases are definitionally equivalent to the
join/meet/complement bases are given, and independence proofs
are given.
Our Sheffer stroke notation is inconsistent  for Otter and
Mace we use "f(x,y)", and when formatting the
equations for presentation we use "(x  y)".
2.3 Finding and Proving the Multiequation Bases
See the v10 paper.
2.4 Are There Simpler Multiequation Bases?
See the v10 paper.
3 Single Axioms
3.1 Generating and Filtering Candidates
See "Single Axiom Searches and Proofs" below.
3.2 Finite Ortholattices
The table Number of Lattices
gives access to listings of the small finite OLs, OMLs, MOLs, and BAs.
3.3 Collecting and Applying Filters
How were the filters found?
3.4 Trying to Prove that Candidates are Single Axioms
See "Single Axiom Searches and Proofs" below.
3.5 Single Axioms for OL, OML, and MOL
f(f(f(f(y,x),f(x,z)),u),f(x,f(f(x,f(f(y,y),y)),z))) = x. % OLSh
f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z))) = x. % OMLSh
f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x. % MOLSh
For comparison, here is one of the BA axioms [12].
f(f(y,f(f(x,y),y)),f(x,f(z,y))) = x. % BASh
Single Axiom Searches and Proofs
4 The Computer Programs
Here is a summary of the programs,
with examples.
Also see the v10 paper.
5 Remarks
See the v10 paper.
References
These references are taken from the v10 paper and the tech. report.

G. Graetzer.
General Lattice Theory.
Brikhauser Verlag, 2nd edition, 1998.

G. Kalmbach.
Orthomodular Lattices.
Academic Press, New York, 1983.

D. Kelly and R. Padmanabhan.
Orthomodular lattices and congruence permutability.
Preprint, 2003.

W. McCune.
MACE 2.0 Reference Manual and Guide.
Tech. Memo ANL/MCSTM249, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, June 2001.

W. McCune.
Mace4 Reference Manual and Guide.
Tech. Memo ANL/MCSTM263, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, August 2003.

W. McCune.
Otter 3.3 Reference Manual.
Tech. Memo ANL/MCSTM263, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, August 2003.

W. McCune and R. Padmanabhan.
Single identities for lattice theory and for weakly associative
lattices.
Algebra Universalis, 36(4):436449, 1996.

W. McCune, R. Padmanabhan, M. A. Rose, and R. Veroff.
Short equational bases for ortholattices: Proofs and countermodels.
Tech. Memo ANL/MCSTM265, Mathematics and Computer Science Division,
Argonne National Laboratory, Argonne, IL, September 2003.

W. McCune, R. Padmanabhan, M. A. Rose, and R. Veroff.
Short equational bases for ortholattices.
Preprint ANL/MCSP10870903, Mathematics and Computer Science
Division, Argonne National Laboratory, Argonne, IL, September 2003.

W. McCune, R. Padmanabhan, and R. Veroff.
Yet another single law for lattices.
Algebra Universalis.
To appear.

W. McCune and O. Shumsky.
IVY: A preprocessor and proof checker for firstorder logic.
In M. Kaufmann, P. Manolios, and J Moore, editors,
ComputerAided Reasoning: ACL2 Case Studies, chapter 16.
Kluwer Academic, 2000.

W. McCune, R. Veroff, B. Fitelson, K. Harris, A. Feist, and L. Wos.
Short single axioms for Boolean algebra.
J. Automated Reasoning, 29(1):116, 2002.

C. A. Meredith and A. N. Prior.
Equational logic.
Notre Dame J. Formal Logic, 9:212226, 1968.

R. Padmanabhan.
Equational theory of algebras with a majority polynomial.
Algebra Universalis, 7(2):273275, 1977.

R. Padmanabhan and R. W. Quackenbush.
Equational theories of algebras with distributive congruences.
Proc. AMS, 41(2):373377, 1973.

M. Pavicic and N. Megill.
Nonorthomodular models for both standard quantum logic and standard
classical logic: Repercussions for quantum computers.
Helv. Phys. Acta, 72(3):189210, 1999.

G. Sutcliffe, C. Suttner, and F. J. Pelletier.
The IJCAR ATP system competition.
J. Automated Reasoning, 28(3):307320, 2002.

G. Szpiro.
Mathematics: Does the proof stack up?
Nature, 242:1213, July 2003.

A. Tarski.
Ein Beitrag zur Axiomatik der Abelschen Gruppen.
Fundamenta Mathematicae, 30:253256, 1938.

R. Veroff.
A shortest 2basis for Boolean algebra in terms of the Sheffer
stroke.
J. Automated Reasoning.
To appear.

R. Veroff.
Using hints to increase the effectiveness of an automated reasoning
program: Case studies.
J. Automated Reasoning, 16(3):223239, 1996.

R. Veroff.
Solving open questions and other challenge problems using proof
sketches.
J. Automated Reasoning, 27(2):157174, 2001.