{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T01:25:22Z","timestamp":1783905922753,"version":"3.55.0"},"reference-count":22,"publisher":"Walter de Gruyter GmbH","issue":"2","license":[{"start":{"date-parts":[[2018,7,1]],"date-time":"2018-07-01T00:00:00Z","timestamp":1530403200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,7,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats: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 [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).<\/jats:p>","DOI":"10.2478\/forma-2018-0017","type":"journal-article","created":{"date-parts":[[2019,1,3]],"date-time":"2019-01-03T12:44:04Z","timestamp":1546519444000},"page":"193-198","source":"Crossref","is-referenced-by-count":2,"title":["On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander"],"prefix":"10.2478","volume":"26","author":[{"given":"Adam","family":"Grabowski","sequence":"first","affiliation":[{"name":"Institute of Informatics , University of Bia\u0142ystok , Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Damian","family":"Sawicki","sequence":"additional","affiliation":[{"name":"Institute of Informatics , University of Bia\u0142ystok , Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2018,12,24]]},"reference":[{"key":"2026071215023404599_j_forma-2018-0017_ref_001_w2aab3b7b9b1b6b1ab1ab1Aa","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, and Karol P\u0105k. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9\u201332, 2018. doi:10.1007\/s10817-017-9440-6.10.1007\/s10817-017-9440-6604425130069070","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026071215023404599_j_forma-2018-0017_ref_002_w2aab3b7b9b1b6b1ab1ab2Aa","unstructured":"[2] Garrett Birkhoff. Lattice Theory. Providence, Rhode Island, New York, 1967."},{"key":"2026071215023404599_j_forma-2018-0017_ref_003_w2aab3b7b9b1b6b1ab1ab3Aa","doi-asserted-by":"crossref","unstructured":"[3] B. I. Dahn. Robbins algebras are Boolean: A revision of McCune\u2019s computer-generated solution of Robbins problem. Journal of Algebra, 208:526\u2013532, 1998.10.1006\/jabr.1998.7467","DOI":"10.1006\/jabr.1998.7467"},{"key":"2026071215023404599_j_forma-2018-0017_ref_004_w2aab3b7b9b1b6b1ab1ab4Aa","doi-asserted-by":"crossref","unstructured":"[4] B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002.10.1017\/CBO9780511809088","DOI":"10.1017\/CBO9780511809088"},{"key":"2026071215023404599_j_forma-2018-0017_ref_005_w2aab3b7b9b1b6b1ab1ab5Aa","doi-asserted-by":"crossref","unstructured":"[5] Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 55:211\u2013221, 2015. doi:10.1007\/s10817-015-9333-5.10.1007\/s10817-015-9333-5","DOI":"10.1007\/s10817-015-9333-5"},{"key":"2026071215023404599_j_forma-2018-0017_ref_006_w2aab3b7b9b1b6b1ab1ab6Aa","doi-asserted-by":"crossref","unstructured":"[6] Adam Grabowski. Lattice theory for rough sets \u2013 a case study with Mizar. Fundamenta Informaticae, 147(2\u20133):223\u2013240, 2016. doi:10.3233\/FI-2016-1406.10.3233\/FI-2016-1406","DOI":"10.3233\/FI-2016-1406"},{"key":"2026071215023404599_j_forma-2018-0017_ref_007_w2aab3b7b9b1b6b1ab1ab7Aa","unstructured":"[7] Adam Grabowski. Robbins algebras vs. Boolean algebras. Formalized Mathematics,9(4): 681\u2013690, 2001."},{"key":"2026071215023404599_j_forma-2018-0017_ref_008_w2aab3b7b9b1b6b1ab1ab8Aa","unstructured":"[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\u2013129. Springer, 2004. doi:10.1007\/978-3-540-27818-4_9. 3rd International Conference on Mathematical Knowledge Management, Bialowieza, Poland, Sep. 19\u201321, 2004.10.1007\/978-3-540-27818-4_9.3rdSep.19212004"},{"key":"2026071215023404599_j_forma-2018-0017_ref_009_w2aab3b7b9b1b6b1ab1ab9Aa","doi-asserted-by":"crossref","unstructured":"[9] Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191\u2013198, 2015. doi:10.1007\/s10817-015-9345-1.10.1007\/s10817-015-9345-1","DOI":"10.1007\/s10817-015-9345-1"},{"key":"2026071215023404599_j_forma-2018-0017_ref_010_w2aab3b7b9b1b6b1ab1ac10Aa","doi-asserted-by":"crossref","unstructured":"[10] Adam Grabowski, Artur Korni\u0142owicz, 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\u201354. IEEE, 2015. doi:10.15439\/2015F229.10.15439\/2015F229","DOI":"10.15439\/2015F229"},{"key":"2026071215023404599_j_forma-2018-0017_ref_011_w2aab3b7b9b1b6b1ab1ac11Aa","doi-asserted-by":"crossref","unstructured":"[11] George Gr\u00e4tzer. General Lattice Theory. Academic Press, New York, 1978.10.1007\/978-3-0348-7633-9","DOI":"10.1007\/978-3-0348-7633-9"},{"key":"2026071215023404599_j_forma-2018-0017_ref_012_w2aab3b7b9b1b6b1ab1ac12Aa","doi-asserted-by":"crossref","unstructured":"[12] George Gr\u00e4tzer. Lattice Theory: Foundation. Birkh\u00e4user, 2011.10.1007\/978-3-0348-0018-1","DOI":"10.1007\/978-3-0348-0018-1"},{"key":"2026071215023404599_j_forma-2018-0017_ref_013_w2aab3b7b9b1b6b1ab1ac13Aa","unstructured":"[13] Violetta Kozarkiewicz and Adam Grabowski. Axiomatization of Boolean algebras based on Sheffer stroke. Formalized Mathematics, 12(3):355\u2013361, 2004."},{"key":"2026071215023404599_j_forma-2018-0017_ref_014_w2aab3b7b9b1b6b1ab1ac14Aa","doi-asserted-by":"crossref","unstructured":"[14] W. McCune, R. Padmanabhan, M. A. Rose, and R. Veroff. Automated discovery of single axioms for ortholattices. Algebra Universalis, 52(4):541\u2013549, 2005.10.1007\/s00012-004-1902-0","DOI":"10.1007\/s00012-004-1902-0"},{"key":"2026071215023404599_j_forma-2018-0017_ref_015_w2aab3b7b9b1b6b1ab1ac15Aa","unstructured":"[15] William McCune. Prover9 and Mace4. 2005\u20132010."},{"key":"2026071215023404599_j_forma-2018-0017_ref_016_w2aab3b7b9b1b6b1ab1ac16Aa","doi-asserted-by":"crossref","unstructured":"[16] William McCune and Ranganathan Padmanabhan. Automated Deduction in Equational Logic and Cubic Curves. Springer-Verlag, Berlin, 1996.10.1007\/3-540-61398-6","DOI":"10.1007\/3-540-61398-6"},{"key":"2026071215023404599_j_forma-2018-0017_ref_017_w2aab3b7b9b1b6b1ab1ac17Aa","doi-asserted-by":"crossref","unstructured":"[17] Ralph McKenzie. Equational bases for lattice theories. Mathematica Scandinavica, 27: 24\u201338, 1970. doi:10.7146\/math.scand.a-10984.10.7146\/math.scand.a-10984","DOI":"10.7146\/math.scand.a-10984"},{"key":"2026071215023404599_j_forma-2018-0017_ref_018_w2aab3b7b9b1b6b1ab1ac18Aa","doi-asserted-by":"crossref","unstructured":"[18] Ranganathan Padmanabhan and Sergiu Rudeanu. Axioms for Lattices and Boolean Algebras. World Scientific Publishers, 2008.10.1142\/7007","DOI":"10.1142\/7007"},{"key":"2026071215023404599_j_forma-2018-0017_ref_019_w2aab3b7b9b1b6b1ab1ac19Aa","unstructured":"[19] Piotr Rudnicki and Josef Urban. Escape to ATP for Mizar. In First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011, 2011."},{"key":"2026071215023404599_j_forma-2018-0017_ref_020_w2aab3b7b9b1b6b1ab1ac20Aa","doi-asserted-by":"crossref","unstructured":"[20] Marlow Sholander. Postulates for distributive lattices. Canadian Journal of Mathematics, 3:28\u201330, 1951. doi:10.4153\/CJM-1951-003-5.10.4153\/CJM-1951-003-5","DOI":"10.4153\/CJM-1951-003-5"},{"key":"2026071215023404599_j_forma-2018-0017_ref_021_w2aab3b7b9b1b6b1ab1ac21Aa","unstructured":"[21] Wioletta Truszkowska and Adam Grabowski. On the two short axiomatizations of ortho-lattices. Formalized Mathematics, 11(3):335\u2013340, 2003."},{"key":"2026071215023404599_j_forma-2018-0017_ref_022_w2aab3b7b9b1b6b1ab1ac22Aa","unstructured":"[22] Stanis\u0142aw \u017bukowski. Introduction to lattice theory. Formalized Mathematics,1(1):215\u2013222, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/26\/2\/article-p193.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2018-0017","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T00:59:40Z","timestamp":1783904380000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2018-0017"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,1]]},"references-count":22,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2018,12,24]]},"published-print":{"date-parts":[[2018,7,1]]}},"alternative-id":["10.2478\/forma-2018-0017"],"URL":"https:\/\/doi.org\/10.2478\/forma-2018-0017","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2018,7,1]]}}}