@MISC{SHEFFER2.MIZ,
  AUTHOR = {{\L}ukaszuk, Aneta and Grabowski, Adam},
  TITLE = {Short {S}heffer Stroke-Based Single Axiom for {B}oolean Algebras},
  SECTION1 = {First Implication},
  SECTION2 = {Second Implication},
  DAY = {31},
  MONTH = {May},
  YEAR = {2004},
  ADDRESS1 = {University of Bia{\l}ystok},
  ADDRESS2 = {University of Bia{\l}ystok},
  SUMMARY = {We continue the description of Boolean algebras in terms of
   the Sheffer stroke as defined in \cite{SHEFFER1.ABS}.
   The single axiomatization for BAs in terms of disjunction
   and negation was shown in \cite{ROBBINS2.ABS}.
   As was checked automatically with the help of automated
   theorem prover Otter, single axiom of the form
   $$(x | ((y | x) | x)) | (y | (z | x)) = y\quad{\rm (Sh1)}$$
   is enough to axiomatize the class of all Boolean algebras
   ($\upharpoonright$ is used
   instead of $|$ in translation of our Mizar article).
   Many theorems in Section 2
   were automatically translated from the Otter proof object.}}

