On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander

[1] 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-6604425130069070Open DOISearch in Google Scholar

[2] Garrett Birkhoff. Lattice Theory. Providence, Rhode Island, New York, 1967.Search in Google Scholar

[3] B. I. Dahn. Robbins algebras are Boolean: A revision of McCune’s computer-generated solution of Robbins problem. Journal of Algebra, 208:526–532, 1998.10.1006/jabr.1998.7467Search in Google Scholar

[4] B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002.10.1017/CBO9780511809088Search in Google Scholar

[5] 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-5Open DOISearch in Google Scholar

[6] Adam Grabowski. Lattice theory for rough sets – a case study with Mizar. Fundamenta Informaticae, 147(2–3):223–240, 2016. doi:10.3233/FI-2016-1406.10.3233/FI-2016-1406Open DOISearch in Google Scholar

[7] Adam Grabowski. Robbins algebras vs. Boolean algebras. Formalized Mathematics,9(4): 681–690, 2001.Search in Google Scholar

[8] 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.10.1007/978-3-540-27818-4_9.3rdSep.19212004Open DOISearch in Google Scholar

[9] Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.10.1007/s10817-015-9345-1Open DOISearch in Google Scholar

[10] 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/2015F229Search in Google Scholar

[11] George Grätzer. General Lattice Theory. Academic Press, New York, 1978.10.1007/978-3-0348-7633-9Search in Google Scholar

[12] George Grätzer. Lattice Theory: Foundation. Birkhäuser, 2011.10.1007/978-3-0348-0018-1Search in Google Scholar

[13] Violetta Kozarkiewicz and Adam Grabowski. Axiomatization of Boolean algebras based on Sheffer stroke. Formalized Mathematics, 12(3):355–361, 2004.Search in Google Scholar

[14] W. McCune, R. Padmanabhan, M. A. Rose, and R. Veroff. Automated discovery of single axioms for ortholattices. Algebra Universalis, 52(4):541–549, 2005.10.1007/s00012-004-1902-0Search in Google Scholar

[15] William McCune. Prover9 and Mace4. 2005–2010.Search in Google Scholar

[16] William McCune and Ranganathan Padmanabhan. Automated Deduction in Equational Logic and Cubic Curves. Springer-Verlag, Berlin, 1996.10.1007/3-540-61398-6Search in Google Scholar

[17] Ralph McKenzie. Equational bases for lattice theories. Mathematica Scandinavica, 27: 24–38, 1970. doi:10.7146/math.scand.a-10984.10.7146/math.scand.a-10984Open DOISearch in Google Scholar

[18] Ranganathan Padmanabhan and Sergiu Rudeanu. Axioms for Lattices and Boolean Algebras. World Scientific Publishers, 2008.10.1142/7007Search in Google Scholar

[19] 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

[20] Marlow Sholander. Postulates for distributive lattices. Canadian Journal of Mathematics, 3:28–30, 1951. doi:10.4153/CJM-1951-003-5.10.4153/CJM-1951-003-5Open DOISearch in Google Scholar

[21] Wioletta Truszkowska and Adam Grabowski. On the two short axiomatizations of ortho-lattices. Formalized Mathematics, 11(3):335–340, 2003.Search in Google Scholar

[22] Stanisław Żukowski. Introduction to lattice theory. Formalized Mathematics,1(1):215–222, 1990.Search in Google Scholar