@MISC{NELSON_1.MIZ,
  AUTHOR = {Grabowski, Adam},
  TITLE = {Two Axiomatizations of {N}elson Algebras},
  SECTION1 = {De Morgan and Quasi-Boolean Lattices},
  SECTION2 = {The Structure and Operators in Nelson Algebras},
  SECTION3 = {The Non-Equational Axiomatization},
  SECTION4 = {Properties of Nelson Algebras},
  SECTION5 = {Alternative Equational Axiomatics by Rasiowa},
  DAY = {19},
  MONTH = {April},
  YEAR = {2015},
  ADDRESS1 = {Institute of Informatics\\ University
    of Bia\l ystok\\ Ciol kowskiego 1M, 15-245 Bia]\l ystok, Poland},
  SUMMARY = {Nelson algebras were first studied by Rasiowa and
  Bia\l ynicki-Birula \cite{RasiowaBirula}
  under the name N-lattices or quasi-pseudo-Boolean algebras.
  Later, in investigations by Monteiro and Brignole
  and \cite{Brignole} the name ``Nelson algebras" was adopted
  -- which is now commonly used
  to show the correspondence with Nelson's paper \cite{Nelson}
  on constructive logic with strong negation.
  \par
  In this article we give the definition and basic properties
  of these algebras according to \cite{RasiowaNonClassical}
  and \cite{Rasiowa:2001}. We start with preliminary section on
  quasi-Boolean algebras (i.e. de Morgan bounded lattices). Later we give
  the axioms in the form of Mizar adjectives with names
  corresponding with those in \cite{Rasiowa:2001}.
  As our main result we give two axiomatizations
  (non-equational and equational)
  and the full formal proof of their equivalence.
  \par
  The second set of equations is rather long but it shows
  the logical flavour of Nelson lattices.
  This formalization aims at the construction of algebraic
  model of rough sets in our future submissions.}}

@BOOK{Rasiowa:2001,
 AUTHOR={Rasiowa, Helena},
 TITLE={Algebraic Models of Logics},
 PUBLISHER={Warsaw University},
 YEAR=2001}

@BOOK{RasiowaNonClassical,
 AUTHOR={Rasiowa, Helena},
 TITLE={An Algebraic Approach to Non-Classical Logics},
 PUBLISHER={North Holland},
 YEAR=1974}

@ARTICLE{Brignole,
 AUTHOR={Brignole, Diana},
 TITLE={Equational Characterization of {N}elson Algebra},
 JOURNAL={Notre Dame Journal of Formal Logic},
 YEAR=1969,
 VOLUME=X,
 NUMBER = 3,
 PAGES={285--297}}

@ARTICLE{RasiowaBirula,
 AUTHOR={Birula-Bia\l ynicki, Andrzej and Rasiowa, Helena},
 TITLE={On the Representation of Quasi-Boolean Algebras},
 JOURNAL={Bulletin de l'Academie Polonaise des Sciences},
 YEAR=1957,
 VOLUME=5,
 PAGES={259--261}}

@ARTICLE{Nelson,
 AUTHOR={Nelson, David},
 TITLE={Constructible Falsity},
 JOURNAL={Journal of Symbolic Logic},
 YEAR=1949,
 VOLUME=14,
 PAGES={16--26}}



