@MISC{LATTBA_1.MIZ,
  AUTHOR = {Ku\'smierowski, Wojciech and Grabowski, Adam},
  TITLE = {Automatization of {T}ernary {B}oolean {A}lgebras},
  SECTION1 = {Preliminaries},
  SECTION2 = {Converting TBAs into Ordinary Binary Boolean Algebras},
  SECTION3 = {Basic Properties of Ternary Operation},
  SECTION4 = {The Rosetta Operation},
  SECTION5 = {Proof that TBA2BAA is Boolean},
  SECTION6 = {Proof that BA2BAA Returns Standard Example of TBA},
  SECTION7 = {Single Axioms for TBA},
  DAY = {30},
  MONTH = {September},
  YEAR = {2021},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  ADDRESS2 = {Institute of Informatics\\University of Bia{\l}ystok\\Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {The main aim of this article is to introduce formally ternary Boolean
  algebras (TBAs) in terms of an abstract ternary operation, and to prove that
  it is equivalent to the ordinary notion of a Boolean algebra, already present
  in the Mizar Mathematical Library. Essentially, this core of this Mizar formalization
  is based on the paper of A.A. Grau "Ternary Boolean Algebras".
  Some of the results were
  proven in the Mizar system with the help of Prover9 proof assistant, 
  so proofs are quite lenghty. They can be subject for subsequent revisions
  to make them more compact.}}