Formalization of Generalized Almost Distributive Lattices

Adam 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 -