On Weakly Associative Lattices and Near Lattices

Damian Sawicki; Adam Grabowski

doi:10.2478/forma-2021-0008

.blurhash-client-img { display: none !important; }

On Weakly Associative Lattices and Near Lattices

Formalized Mathematics

Volume 29 (2021): Issue 2 (July 2021)

By: Damian Sawicki and Adam Grabowski

Open Access

|Dec 2021

Abstract

Summary. The main aim of this article is to introduce formally two generalizations of lattices, namely weakly associative lattices and near lattices, which can be obtained from the former by certain weakening of the usual well-known axioms. We show selected propositions devoted to weakly associative lattices and near lattices from Chapter 6 of [15], dealing also with alternative versions of classical axiomatizations. Some of the results were proven in the Mizar [1], [2] system with the help of Prover9 [14] proof assistant.

References

Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.10.1007/978-3-319-20615-8_17
Search in Google Scholar Back to article
Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.10.1007/s10817-017-9440-6604425130069070
Search in Google Scholar Back to article
Garrett Birkhoff. Lattice Theory. Providence, Rhode Island, New York, 1967.
Search in Google Scholar Back to article
B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002.10.1017/CBO9780511809088
Search in Google Scholar Back to article
Ervin Fried and George Gr¨atzer. Some examples of weakly associative lattices. Colloquium Mathematicum, 27:215–221, 1973. doi:10.4064/cm-27-2-215-221.10.4064/cm-27-2-215-221
Search in Google Scholar Back to article
Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 55:211–221, 2015. doi:10.1007/s10817-015-9333-5.10.1007/s10817-015-9333-5
Search in Google Scholar Back to article
Adam Grabowski and Markus Moschner. Managing heterogeneous theories within a mathematical knowledge repository. In Andrea Asperti, Grzegorz Bancerek, and Andrzej Trybulec, editors, Mathematical Knowledge Management Proceedings, volume 3119 of Lecture Notes in Computer Science, pages 116–129. Springer, 2004. doi:10.1007/978-3-540-27818-4_9. 3rd International Conference on Mathematical Knowledge Management, Bialowieza, Poland, Sep. 19–21, 2004.
Search in Google Scholar Back to article
Adam Grabowski and Damian Sawicki. On two alternative axiomatizations of lattices by McKenzie and Sholander. Formalized Mathematics, 26(2):193–198, 2018. doi:10.2478/forma-2018-0017.10.2478/forma-2018-0017
Search in Google Scholar Back to article
Adam Grabowski and Christoph Schwarzweller. Translating mathematical vernacular into knowledge repositories. In Michael Kohlhase, editor, Mathematical Knowledge Management, volume 3863 of Lecture Notes in Computer Science, pages 49–64. Springer, 2006. doi:https://doi.org/10.1007/11618027_4. 4th International Conference on Mathematical Knowledge Management, Bremen, Germany, MKM 2005, July 15–17, 2005, Revised Selected Papers.
Search in Google Scholar Back to article
Adam Grabowski, Artur Korniłowicz, and Christoph Schwarzweller. Equality in computer proof-assistants. In Ganzha, Maria and Maciaszek, Leszek and Paprzycki, Marcin, editor, Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, volume 5 of ACSIS-Annals of Computer Science and Information Systems, pages 45–54. IEEE, 2015. doi:10.15439/2015F229.10.15439/2015F229
Search in Google Scholar Back to article
George Gr¨atzer. General Lattice Theory. Academic Press, New York, 1978.10.1007/978-3-0348-7633-9
Search in Google Scholar Back to article
George Gr¨atzer. Lattice Theory: Foundation. Birkh¨auser, 2011.10.1007/978-3-0348-0018-1
Search in Google Scholar Back to article
Dominik Kulesza and Adam Grabowski. Formalization of quasilattices. Formalized Mathematics, 28(2):217–225, 2020. doi:10.2478/forma-2020-0019.10.2478/forma-2020-0019
Search in Google Scholar Back to article
William McCune. Prover9 and Mace4. 2005–2010.
Search in Google Scholar Back to article
William McCune and Ranganathan Padmanabhan. Automated Deduction in Equational Logic and Cubic Curves. Springer-Verlag, Berlin, 1996.10.1007/3-540-61398-6
Search in Google Scholar Back to article
Ranganathan Padmanabhan and Sergiu Rudeanu. Axioms for Lattices and Boolean Algebras. World Scientific Publishers, 2008.10.1142/7007
Search in Google Scholar Back to article
Piotr Rudnicki and Josef Urban. Escape to ATP for Mizar. In First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011, 2011.
Search in Google Scholar Back to article
Stanisław łukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215–222, 1990.
Search in Google Scholar Back to article

Articles in this issue

DOI: https://doi.org/10.2478/forma-2021-0008 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 77 - 85

Accepted on: Jun 30, 2021

Published on: Dec 30, 2021

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Keywords:

68V20,

06B05,

06B75

Related subjects:

Computer sciences,

Computer sciences, other,

Mathematics,

General mathematics

© 2021 Damian Sawicki, Adam Grabowski, published by University of Białystok
This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.

Volume 29 (2021): Issue 2 (July 2021)