@MISC{ROBBINS3.MIZ,
  AUTHOR = {Grabowski, Adam and Moschner, Markus},
  TITLE = {Formalization of Ortholattices via~Orthoposets},
  SECTION1 = {Another Short Axiomatization of Lattices},
  SECTION2 = {Orthoposets},
  SECTION3 = {Merging Relational Structures and Lattice Structures Together},
  SECTION4 = {Binary Approach to Ortholattices},
  SECTION5 = {Lemmas},
  SECTION6 = {Structure Extensions},
  SECTION7 = {Extending Orthocomplemented Lattice Structure},
  DAY = {28},
  MONTH = {December},
  YEAR = {2004},
  ADDRESS1 = {University of Bia{\l}ystok},
  ADDRESS2 = {University of Vienna},
  SUMMARY = {There are two approaches to lattices
  used in the Mizar Mathematical Library: on the one hand, these
  structures are based on the set
  with two binary operations (with an equational characterization
  as in \cite{LATTICES.ABS}). On the other hand, we may look at them
  as at relational structures (posets -- see \cite{ORDERS_1.ABS}).
  As the main result of this article we can state that the Mizar
  formalization enables us to use both approaches simultaneously
  (Section 3). This is especially useful because most of
  lemmas on ortholattices in the literature
  are stated in the poset setting, so we cannot use equational theorem
  provers in a straightforward way.
  We give also short equational characterization of lattices via four axioms
  (as it was done in \cite{McCune:2005} with the help of the Otter prover).
  Some corresponding results about ortholattices are also formalized.}}


@ARTICLE{McCune:2005,
       AUTHOR = {McCune, W. and Padmanabhan, R. and Rose, M. A. and Veroff, R.},
      JOURNAL = {Algebra Universalis},
         YEAR = {2005},
       VOLUME = {52(4)},
        PAGES = {541--549}}}