<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>The main aim of this article is to introduce formally ternary Boolean algebras (TBAs) in terms of an abstract ternary operation, and to show their connection with the ordinary notion of a Boolean algebra, already present in the Mizar Mathematical Library [2]. Essentially, the core of this Mizar [1] formalization is based on the paper of A.A. Grau “Ternary Boolean Algebras” [7]. The main result is the single axiom for this class of lattices [12]. This is the continuation of the articles devoted to various equivalent axiomatizations of Boolean algebras: following Huntington [8] in terms of the binary sum and the complementation useful in the formalization of the Robbins problem [5], in terms of Sheffer stroke [9]. The classical definition ([6], [3]) can be found in [15] and its formalization is described in [4].</p>
<p>Similarly as in the case of recent formalizations of WA-lattices [14] and quasilattices [10], some of the results were proven in the Mizar system with the help of Prover9 [13], [11] proof assistant, so proofs are quite lengthy. They can be subject for subsequent revisions to make them more compact.</p>
</abstract>

The main aim of this article is to introduce formally ternary Boolean algebras (TBAs) in terms of an abstract ternary operation, and to show their connection with the ordinary notion of a Boolean algebra, already present in the Mizar Mathematical Library [2]. Essentially, the core of this Mizar [1] formalization is based on the paper of A.A. Grau “Ternary Boolean Algebras” [7]. The main result is the single axiom for this class of lattices [12]. This is the continuation of the articles devoted to various equivalent axiomatizations of Boolean algebras: following Huntington [8] in terms of the binary sum and the complementation useful in the formalization of the Robbins problem [5], in terms of Sheffer stroke [9]. The classical definition ([6], [3]) can be found in [15] and its formalization is described in [4].
Similarly as in the case of recent formalizations of WA-lattices [14] and quasilattices [10], some of the results were proven in the Mizar system with the help of Prover9 [13], [11] proof assistant, so proofs are quite lengthy. They can be subject for subsequent revisions to make them more compact.

Automatization of Ternary Boolean Algebras

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"Automatization of Ternary Boolean Algebras"}

The main aim of this article is to introduce formally ternary Boolean algebras (TBAs) in terms of an abstract ternary operation, and to show their connection...

Automatization of Ternary Boolean Algebras

Data publikacji: 09 lip 2022

Zakres stron: 153 - 159

Przyjęty: 30 wrz 2021

DOI: https://doi.org/10.2478/forma-2021-0015

Słowa kluczowe
ternary Boolean algebra, single axiom system, lattice

© 2022 Wojciech Kuśmierowski et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Automatization of Ternary Boolean Algebras

Data publikacji: 09 lip 2022

Zakres stron: 153 - 159

Przyjęty: 30 wrz 2021

DOI: https://doi.org/10.2478/forma-2021-0015

Słowa kluczoweternary Boolean algebra, single axiom system, lattice

© 2022 Wojciech Kuśmierowski et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Słowa kluczowe
ternary Boolean algebra, single axiom system, lattice