@MISC{LATTAD_1.MIZ,
  AUTHOR = {Grabowski, Adam},
  TITLE = {Formalization of Generalized Almost Distributive Lattices},
  SECTION1 = {Preliminaries},
  SECTION2 = {Almost Distributive Lattices},
  SECTION3 = {Properties of Almost Distributive Lattices},
  SECTION4 = {Generalization of Almost Distributive Lattices},
  SECTION5 = {Order Properties of the Generated Relation on GADLs},
  SECTION6 = {Formalization of {R}ao et al.'s paper},
  SECTION7 = {Generalized Almost Distributive Lattices with Zero},
  SECTION8 = {Constructing Examples of Almost Distributive Lattices},
  ACKNOWLEDEGEMENT = {The author want to express his gratitude to the
  anonymous referee for his work on the last section of this article;
  although I didn't want to add more concrete examples than the
  simplest ones, these additional constructions proposed by the referee
  really complete the Mizar article as a faithful translation of
  the Rao's results, in the same time suggesting
  possible improvements of the Mizar Mathematical Library.},
  DAY = {26},
  MONTH = {September},
  YEAR = {2014},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Akademicka 2, 15-267 Bia{\l}ystok\\Poland},
  SUMMARY = {Almost Distributive Lattices (ADL) are structures defined by
  Swamy and Rao \cite{SwamyRao1981}
  as a common abstraction of some generalizations
  of a Boolean algebra. In our paper, we deal with a certain further
  generalization of ADLs, namely Generalized Almost Distributive Lattices.
  Our main aim was to give the formal counterpart of this structure
  and we succeeded formalizing all items from the Section 3 of {R}ao et al.'s paper
  \cite{GADL:2009}. Essentially GADLs need not be neither $\vee$-
  nor $\wedge$-commutative and $\wedge$-associative; consequently
  not all forms of absorption identities hold.\par
  We characterized some necessary and sufficient conditions for
  commutativity and distributivity, we defined also the class of
  GADLs with zero element. We tried to use as much attributes and
  clusters registration as possible, hence many identities are
  expressed in terms of adjectives; also some generalizations
  of well-known notions from lattice theory formalized within the
  Mizar Mathematical Library were proposed. At the end some important
  examples from Rao's paper were introduced.}}

@article{SwamyRao1981,
  author    = {Swamy, U.M. and Rao, G.C.},
  title     = {Almost Distributive Lattices},
  journal   = {Journal of Australian Mathematical Society},
  volume    = {31},
  year      = {1981},
  pages     = {77--91}}

@article{GADL:2009,
  author    = {Rao, G.C. and Bandaru, R.K. and Rafi, N.},
  title     = {Generalized Almost Distributive Lattices -- {I}},
  journal   = {Southeast Asian Bulletin of Mathematics},
  volume    = {33},
  year      = {2009},
  pages     = {1175--1188}}
