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.

Son of BirdBrain, the Web-based 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.       % OL-Sh
    f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z))) = x.       % OML-Sh
    f(f(y,x),f(f(f(x,x),z),f(f(f(f(f(x,y),z),z),x),f(x,u)))) = x.  % MOL-Sh
For comparison, here is one of the BA axioms [12]. 
    f(f(y,f(f(x,y),y)),f(x,f(z,y))) = x.   % BA-Sh

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.
  1. G. Graetzer. General Lattice Theory. Brikhauser Verlag, 2nd edition, 1998.
  2. G. Kalmbach. Orthomodular Lattices. Academic Press, New York, 1983.
  3. D. Kelly and R. Padmanabhan. Orthomodular lattices and congruence permutability. Preprint, 2003.
  4. W. McCune. MACE 2.0 Reference Manual and Guide. Tech. Memo ANL/MCS-TM-249, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, June 2001.
  5. W. McCune. Mace4 Reference Manual and Guide. Tech. Memo ANL/MCS-TM-263, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, August 2003.
  6. W. McCune. Otter 3.3 Reference Manual. Tech. Memo ANL/MCS-TM-263, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, August 2003.
  7. W. McCune and R. Padmanabhan. Single identities for lattice theory and for weakly associative lattices. Algebra Universalis, 36(4):436--449, 1996.
  8. W. McCune, R. Padmanabhan, M. A. Rose, and R. Veroff. Short equational bases for ortholattices: Proofs and countermodels. Tech. Memo ANL/MCS-TM-265, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, September 2003.
  9. W. McCune, R. Padmanabhan, M. A. Rose, and R. Veroff. Short equational bases for ortholattices. Preprint ANL/MCS-P1087-0903, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, September 2003.
  10. W. McCune, R. Padmanabhan, and R. Veroff. Yet another single law for lattices. Algebra Universalis. To appear.
  11. W. McCune and O. Shumsky. IVY: A preprocessor and proof checker for first-order logic. In M. Kaufmann, P. Manolios, and J Moore, editors, Computer-Aided Reasoning: ACL2 Case Studies, chapter 16. Kluwer Academic, 2000.
  12. W. McCune, R. Veroff, B. Fitelson, K. Harris, A. Feist, and L. Wos. Short single axioms for Boolean algebra. J. Automated Reasoning, 29(1):1--16, 2002.
  13. C. A. Meredith and A. N. Prior. Equational logic. Notre Dame J. Formal Logic, 9:212--226, 1968.
  14. R. Padmanabhan. Equational theory of algebras with a majority polynomial. Algebra Universalis, 7(2):273--275, 1977.
  15. R. Padmanabhan and R. W. Quackenbush. Equational theories of algebras with distributive congruences. Proc. AMS, 41(2):373--377, 1973.
  16. M. Pavicic and N. Megill. Non-orthomodular models for both standard quantum logic and standard classical logic: Repercussions for quantum computers. Helv. Phys. Acta, 72(3):189--210, 1999.
  17. G. Sutcliffe, C. Suttner, and F. J. Pelletier. The IJCAR ATP system competition. J. Automated Reasoning, 28(3):307--320, 2002.
  18. G. Szpiro. Mathematics: Does the proof stack up? Nature, 242:12--13, July 2003.
  19. A. Tarski. Ein Beitrag zur Axiomatik der Abelschen Gruppen. Fundamenta Mathematicae, 30:253--256, 1938.
  20. R. Veroff. A shortest 2-basis for Boolean algebra in terms of the Sheffer stroke. J. Automated Reasoning. To appear.
  21. R. Veroff. Using hints to increase the effectiveness of an automated reasoning program: Case studies. J. Automated Reasoning, 16(3):223--239, 1996.
  22. R. Veroff. Solving open questions and other challenge problems using proof sketches. J. Automated Reasoning, 27(2):157--174, 2001.