# Formalization of Generalized Almost Distributive Lattices

Formalized Mathematics (2014)

- Volume: 22, Issue: 3, page 257-267
- ISSN: 1426-2630

## Access Full Article

top## Abstract

top## How to cite

topAdam Grabowski. "Formalization of Generalized Almost Distributive Lattices." Formalized Mathematics 22.3 (2014): 257-267. <http://eudml.org/doc/270798>.

@article{AdamGrabowski2014,

abstract = {Almost Distributive Lattices (ADL) are structures defined by Swamy and Rao [14] as a common abstraction of some generalizations of the Boolean algebra. In our paper, we deal with a certain further generalization of ADLs, namely the Generalized Almost Distributive Lattices (GADL). Our main aim was to give the formal counterpart of this structure and we succeeded formalizing all items from the Section 3 of Rao et al.’s paper [13]. Essentially among GADLs we can find structures which are neither V-commutative nor Λ-commutative (resp., Λ-commutative); consequently not all forms of absorption identities hold. We characterized some necessary and sufficient conditions for commutativity and distributivity, we also defined the class of GADLs with zero element. We tried to use as much attributes and cluster registrations as possible, hence many identities are expressed in terms of adjectives; also some generalizations of wellknown notions from lattice theory [11] formalized within the Mizar Mathematical Library were proposed. Finally, some important examples from Rao’s paper were introduced. We construct the example of GADL which is not an ADL. Mechanization of proofs in this specific area could be a good starting point towards further generalization of lattice theory [10] with the help of automated theorem provers [8].},

author = {Adam Grabowski},

journal = {Formalized Mathematics},

keywords = {almost distributive lattices; generalized almost distributive lattices; lattice identities; formalized mathematics; formalization of lattices},

language = {eng},

number = {3},

pages = {257-267},

title = {Formalization of Generalized Almost Distributive Lattices},

url = {http://eudml.org/doc/270798},

volume = {22},

year = {2014},

}

TY - JOUR

AU - Adam Grabowski

TI - Formalization of Generalized Almost Distributive Lattices

JO - Formalized Mathematics

PY - 2014

VL - 22

IS - 3

SP - 257

EP - 267

AB - Almost Distributive Lattices (ADL) are structures defined by Swamy and Rao [14] as a common abstraction of some generalizations of the Boolean algebra. In our paper, we deal with a certain further generalization of ADLs, namely the Generalized Almost Distributive Lattices (GADL). Our main aim was to give the formal counterpart of this structure and we succeeded formalizing all items from the Section 3 of Rao et al.’s paper [13]. Essentially among GADLs we can find structures which are neither V-commutative nor Λ-commutative (resp., Λ-commutative); consequently not all forms of absorption identities hold. We characterized some necessary and sufficient conditions for commutativity and distributivity, we also defined the class of GADLs with zero element. We tried to use as much attributes and cluster registrations as possible, hence many identities are expressed in terms of adjectives; also some generalizations of wellknown notions from lattice theory [11] formalized within the Mizar Mathematical Library were proposed. Finally, some important examples from Rao’s paper were introduced. We construct the example of GADL which is not an ADL. Mechanization of proofs in this specific area could be a good starting point towards further generalization of lattice theory [10] with the help of automated theorem provers [8].

LA - eng

KW - almost distributive lattices; generalized almost distributive lattices; lattice identities; formalized mathematics; formalization of lattices

UR - http://eudml.org/doc/270798

ER -

## References

top- [1] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Formalized Mathematics, 6(1):93-107, 1997.
- [2] Józef Białas. Group and field definitions. Formalized Mathematics, 1(3):433-439, 1990.
- [3] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.
- [4] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.
- [5] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
- [6] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.
- [7] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
- [8] Adam Grabowski and Markus Moschner. Managing heterogeneous theories within a mathematical knowledge repository. In Andrea Asperti, Grzegorz Bancerek, and Andrzej Trybulec, editors, Mathematical Knowledge Management Proceedings, volume 3119 of Lecture Notes in Computer Science, pages 116-129. Springer, 2004. 3rd International Conference on Mathematical Knowledge Management, Bialowieza, Poland, Sep. 19-21, 2004. Zbl1108.68589
- [9] Adam Grabowski and Markus Moschner. Formalization of ortholattices via orthoposets. Formalized Mathematics, 13(1):189-197, 2005.
- [10] George Gr¨atzer. General Lattice Theory. Academic Press, New York, 1978.
- [11] George Gr¨atzer. Lattice Theory: Foundation. Birkh¨auser, 2011.
- [12] Eliza Niewiadomska and Adam Grabowski. Introduction to formal preference spaces. Formalized Mathematics, 21(3):223-233, 2013. doi:10.2478/forma-2013-0024.[Crossref] Zbl1299.91036
- [13] G.C. Rao, R.K. Bandaru, and N. Rafi. Generalized almost distributive lattices - I. Southeast Asian Bulletin of Mathematics, 33:1175-1188, 2009. Zbl1212.06029
- [14] U.M. Swamy and G.C. Rao. Almost distributive lattices. Journal of Australian Mathematical Society, 31:77-91, 1981. Zbl0473.06008
- [15] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25-34, 1990.
- [16] Wojciech A. Trybulec. Partially ordered sets. Formalized Mathematics, 1(2):313-319, 1990.
- [17] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski - Zorn lemma. Formalized Mathematics, 1(2):387-393, 1990.
- [18] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
- [19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.
- [20] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990.
- [21] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Formalized Mathematics, 1(1):85-89, 1990.
- [22] Stanisław Zukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215-222, 1990.

## NotesEmbed ?

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