Orthomodular Lattices

Elżbieta Mądra; Adam Grabowski

Formalized Mathematics (2008)

  • Volume: 16, Issue: 3, page 277-282
  • ISSN: 1426-2630

Abstract

top
The main result of the article is the solution to the problem of short axiomatizations of orthomodular ortholattices. Based on EQP/Otter results [10], we gave a set of three equations which is equivalent to the classical, much longer equational basis of such a class. Also the basic example of the lattice which is not orthomodular, i.e. benzene (or B6) is defined in two settings - as a relational structure (poset) and as a lattice.As a preliminary work, we present the proofs of the dependence of other axiomatizations of ortholattices. The formalization of the properties of orthomodular lattices follows [4].

How to cite

top

Elżbieta Mądra, and Adam Grabowski. "Orthomodular Lattices." Formalized Mathematics 16.3 (2008): 277-282. <http://eudml.org/doc/267071>.

@article{ElżbietaMądra2008,
abstract = {The main result of the article is the solution to the problem of short axiomatizations of orthomodular ortholattices. Based on EQP/Otter results [10], we gave a set of three equations which is equivalent to the classical, much longer equational basis of such a class. Also the basic example of the lattice which is not orthomodular, i.e. benzene (or B6) is defined in two settings - as a relational structure (poset) and as a lattice.As a preliminary work, we present the proofs of the dependence of other axiomatizations of ortholattices. The formalization of the properties of orthomodular lattices follows [4].},
author = {Elżbieta Mądra, Adam Grabowski},
journal = {Formalized Mathematics},
language = {eng},
number = {3},
pages = {277-282},
title = {Orthomodular Lattices},
url = {http://eudml.org/doc/267071},
volume = {16},
year = {2008},
}

TY - JOUR
AU - Elżbieta Mądra
AU - Adam Grabowski
TI - Orthomodular Lattices
JO - Formalized Mathematics
PY - 2008
VL - 16
IS - 3
SP - 277
EP - 282
AB - The main result of the article is the solution to the problem of short axiomatizations of orthomodular ortholattices. Based on EQP/Otter results [10], we gave a set of three equations which is equivalent to the classical, much longer equational basis of such a class. Also the basic example of the lattice which is not orthomodular, i.e. benzene (or B6) is defined in two settings - as a relational structure (poset) and as a lattice.As a preliminary work, we present the proofs of the dependence of other axiomatizations of ortholattices. The formalization of the properties of orthomodular lattices follows [4].
LA - eng
UR - http://eudml.org/doc/267071
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  2. [2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  3. [3] Grzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719-725, 1991. 
  4. [4] Ladislav Beran. Orthomodular Lattices. Algebraic Approach. Academiai Kiado, 1984. 
  5. [5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  6. [6] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  7. [7] Adam Grabowski. Robbins algebras vs. Boolean algebras. Formalized Mathematics, 9(4):681-690, 2001. Zbl0984.06500
  8. [8] Adam Grabowski and Robert Milewski. Boolean posets, posets under inclusion and products of relational structures. Formalized Mathematics, 6(1):117-121, 1997. 
  9. [9] Adam Grabowski and Markus Moschner. Formalization of ortholattices via orthoposets. Formalized Mathematics, 13(1):189-197, 2005. 
  10. [10] W. McCune, R. Padmanabhan, M. A. Rose, and R. Veroff. Automated discovery of single axioms for ortholattices. Algebra Universalis, 52(4):541-549, 2005. Zbl1084.06007
  11. [11] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25-34, 1990. 
  12. [12] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski - Zorn lemma. Formalized Mathematics, 1(2):387-393, 1990. 
  13. [13] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  14. [14] Stanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215-222, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.