<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

Data publikacji: 24 gru 2018

Zakres stron: 193 - 198

Przyjęty: 29 cze 2018

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

Słowa kluczowe
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

Data publikacji: 24 gru 2018

Zakres stron: 193 - 198

Przyjęty: 29 cze 2018

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

Słowa kluczowelattice, 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.

Słowa kluczowe
lattice, distributive lattice, lattice axioms