<abstract xmlns="http://www.w3.org/1999/xhtml"><p>The main result of the article is to prove formally that two sets of axioms, proposed by McKenzie and Sholander, axiomatize lattices and distributive lattices, respectively. In our Mizar article we used proof objects generated by Prover9. We continue the work started in <xref ref-type="bibr" rid="j_forma-2018-0017_ref_007_w2aab3b7b9b1b6b1ab1ab7Aa">[7]</xref>, <xref ref-type="bibr" rid="j_forma-2018-0017_ref_021_w2aab3b7b9b1b6b1ab1ac21Aa">[21]</xref>, and <xref ref-type="bibr" rid="j_forma-2018-0017_ref_013_w2aab3b7b9b1b6b1ab1ac13Aa">[13]</xref> of developing lattice theory as initialized in <xref ref-type="bibr" rid="j_forma-2018-0017_ref_022_w2aab3b7b9b1b6b1ab1ac22Aa">[22]</xref> as a formal counterpart of <xref ref-type="bibr" rid="j_forma-2018-0017_ref_011_w2aab3b7b9b1b6b1ab1ac11Aa">[11]</xref>. Complete formal proofs can be found in the Mizar source code of this article available in the Mizar Mathematical Library (MML).</p></abstract>

The main result of the article is to prove formally that two sets of axioms, proposed by McKenzie and Sholander, axiomatize lattices and distributive lattices, respectively. In our Mizar article we used proof objects generated by Prover9. We continue the work started in [7], [21], and [13] of developing lattice theory as initialized in [22] as a formal counterpart of [11]. Complete formal proofs can be found in the Mizar source code of this article available in the Mizar Mathematical Library (MML).

On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander"}

The main result of the article is to prove formally that two sets of axioms, proposed by McKenzie and Sholander, axiomatize lattices and distributive lattices,...

On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander

Pubblicato online: 24 dic 2018

Pagine: 193 - 198

Accettato: 29 giu 2018

DOI: https://doi.org/10.2478/forma-2018-0017

Parole chiave
lattice, distributive lattice, lattice axioms

© 2018 Adam Grabowski et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander

Pubblicato online: 24 dic 2018

Pagine: 193 - 198

Accettato: 29 giu 2018

DOI: https://doi.org/10.2478/forma-2018-0017

Parole chiavelattice, distributive lattice, lattice axioms

© 2018 Adam Grabowski et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Parole chiave
lattice, distributive lattice, lattice axioms