{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,12]],"date-time":"2026-07-12T23:07:42Z","timestamp":1783897662823,"version":"3.55.0"},"reference-count":15,"publisher":"Walter de Gruyter GmbH","issue":"4","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,12,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>The main aim of this article is to introduce formally ternary Boolean algebras (TBAs) in terms of an abstract ternary operation, and to show their connection with the ordinary notion of a Boolean algebra, already present in the Mizar Mathematical Library [2]. Essentially, the core of this Mizar [1] formalization is based on the paper of A.A. Grau \u201cTernary Boolean Algebras\u201d [7]. The main result is the single axiom for this class of lattices [12]. This is the continuation of the articles devoted to various equivalent axiomatizations of Boolean algebras: following Huntington [8] in terms of the binary sum and the complementation useful in the formalization of the Robbins problem [5], in terms of Sheffer stroke [9]. The classical definition ([6], [3]) can be found in [15] and its formalization is described in [4].<\/jats:p>\n                  <jats:p>Similarly as in the case of recent formalizations of WA-lattices [14] and quasilattices [10], some of the results were proven in the Mizar system with the help of Prover9 [13], [11] proof assistant, so proofs are quite lengthy. They can be subject for subsequent revisions to make them more compact.<\/jats:p>","DOI":"10.2478\/forma-2021-0015","type":"journal-article","created":{"date-parts":[[2022,7,9]],"date-time":"2022-07-09T16:34:12Z","timestamp":1657384452000},"page":"153-159","source":"Crossref","is-referenced-by-count":1,"title":["Automatization of Ternary Boolean Algebras"],"prefix":"10.2478","volume":"29","author":[{"given":"Wojciech","family":"Ku\u015bmierowski","sequence":"first","affiliation":[{"name":"Institute of Computer Science , University of Bia\u0142ystok , Cio\u0142kowskiego 1M, 15-245 Bia\u0142ystok , Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Adam","family":"Grabowski","sequence":"additional","affiliation":[{"name":"Institute of Computer Science , University of Bia\u0142ystok , Cio\u0142kowskiego 1M, 15-245 Bia\u0142ystok , Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2022,7,9]]},"reference":[{"key":"2026071215073871620_j_forma-2021-0015_ref_001","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, 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\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-8_17.","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026071215073871620_j_forma-2021-0015_ref_002","doi-asserted-by":"crossref","unstructured":"[2] 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.","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026071215073871620_j_forma-2021-0015_ref_003","doi-asserted-by":"crossref","unstructured":"[3] B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002.10.1017\/CBO9780511809088","DOI":"10.1017\/CBO9780511809088"},{"key":"2026071215073871620_j_forma-2021-0015_ref_004","doi-asserted-by":"crossref","unstructured":"[4] Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 55:211\u2013221, 2015. doi:10.1007\/s10817-015-9333-5.","DOI":"10.1007\/s10817-015-9333-5"},{"key":"2026071215073871620_j_forma-2021-0015_ref_005","unstructured":"[5] Adam Grabowski. Robbins algebras vs. Boolean algebras. Formalized Mathematics, 9(4): 681\u2013690, 2001."},{"key":"2026071215073871620_j_forma-2021-0015_ref_006","doi-asserted-by":"crossref","unstructured":"[6] 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":"2026071215073871620_j_forma-2021-0015_ref_007","doi-asserted-by":"crossref","unstructured":"[7] Albert A. Grau. Ternary Boolean algebra. Bulletin of the American Mathematical Society, 53(6):567\u2013572, 1947. doi:bams\/1183510797.","DOI":"10.1090\/S0002-9904-1947-08834-0"},{"key":"2026071215073871620_j_forma-2021-0015_ref_008","doi-asserted-by":"crossref","unstructured":"[8] E. V. Huntington. New sets of independent postulates for the algebra of logic, with special reference to Whitehead and Russell\u2019s Principia Mathematica. Trans. AMS, 35:274\u2013304, 1933.10.1090\/S0002-9947-1933-1501684-X","DOI":"10.1090\/S0002-9947-1933-1501684-X"},{"key":"2026071215073871620_j_forma-2021-0015_ref_009","unstructured":"[9] Violetta Kozarkiewicz and Adam Grabowski. Axiomatization of Boolean algebras based on Sheffer stroke. Formalized Mathematics, 12(3):355\u2013361, 2004."},{"key":"2026071215073871620_j_forma-2021-0015_ref_010","doi-asserted-by":"crossref","unstructured":"[10] Dominik Kulesza and Adam Grabowski. Formalization of quasilattices. Formalized Mathematics, 28(2):217\u2013225, 2020. doi:10.2478\/forma-2020-0019.","DOI":"10.2478\/forma-2020-0019"},{"key":"2026071215073871620_j_forma-2021-0015_ref_011","doi-asserted-by":"crossref","unstructured":"[11] 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":"2026071215073871620_j_forma-2021-0015_ref_012","doi-asserted-by":"crossref","unstructured":"[12] Ranganathan Padmanabhan and William McCune. Computers and Mathematics with Applications, 29(2):13\u201316, 1995.10.1016\/0898-1221(94)00213-5","DOI":"10.1016\/0898-1221(94)00213-5"},{"key":"2026071215073871620_j_forma-2021-0015_ref_013","doi-asserted-by":"crossref","unstructured":"[13] Ranganathan Padmanabhan and Sergiu Rudeanu. Axioms for Lattices and Boolean Algebras. World Scientific Publishers, 2008.10.1142\/7007","DOI":"10.1142\/7007"},{"key":"2026071215073871620_j_forma-2021-0015_ref_014","doi-asserted-by":"crossref","unstructured":"[14] Damian Sawicki and Adam Grabowski. On weakly associative lattices and near lattices. Formalized Mathematics, 29(2):77\u201385, 2021. doi:10.2478\/forma-2021-0008.","DOI":"10.2478\/forma-2021-0008"},{"key":"2026071215073871620_j_forma-2021-0015_ref_015","unstructured":"[15] Stanis\u0142aw \u017bukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215\u2013222, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2021-0015","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,12]],"date-time":"2026-07-12T22:55:57Z","timestamp":1783896957000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2021-0015"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,1]]},"references-count":15,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2022,7,9]]},"published-print":{"date-parts":[[2021,12,1]]}},"alternative-id":["10.2478\/forma-2021-0015"],"URL":"https:\/\/doi.org\/10.2478\/forma-2021-0015","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12,1]]}}}