{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T10:03:26Z","timestamp":1771063406691,"version":"3.50.1"},"reference-count":17,"publisher":"Walter de Gruyter GmbH","issue":"2","license":[{"start":{"date-parts":[[2016,6,1]],"date-time":"2016-06-01T00:00:00Z","timestamp":1464739200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,6,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p>In our earlier article [12], the first part of axioms of geometry proposed by Alfred Tarski [14] was formally introduced by means of Mizar proof assistant [9]. We defined a structure <jats:monospace>TarskiPlane<\/jats:monospace> with the following predicates:\n<jats:list list-type=\"bullet\">\n                     <jats:list-item>\n                        <jats:p>of betweenness <jats:monospace>between<\/jats:monospace> (a ternary relation),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>of congruence of segments <jats:monospace>equiv<\/jats:monospace> (quarternary relation),<\/jats:p>\n                     <\/jats:list-item>\n                  <\/jats:list>\nwhich satisfy the following properties:\n<jats:list list-type=\"bullet\">\n                     <jats:list-item>\n                        <jats:p>congruence symmetry (A1),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>congruence equivalence relation (A2),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>congruence identity (A3),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>segment construction (A4),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>SAS (A5),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>betweenness identity (A6),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>Pasch (A7).<\/jats:p>\n                     <\/jats:list-item>\n                  <\/jats:list>\nAlso a simple model, which satisfies these axioms, was previously constructed, and described in [6]. In this paper, we deal with four remaining axioms, namely:\n<jats:list list-type=\"bullet\">\n                     <jats:list-item>\n                        <jats:p>the lower dimension axiom (A8),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>the upper dimension axiom (A9),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>the Euclid axiom (A10),<\/jats:p>\n                     <\/jats:list-item>\n                     <jats:list-item>\n                        <jats:p>the continuity axiom (A11).<\/jats:p>\n                     <\/jats:list-item>\n                  <\/jats:list>\nThey were introduced in the form of Mizar attributes. Additionally, the relation of congruence of triangles <jats:monospace>cong<\/jats:monospace> is introduced via congruence of sides (SSS).<\/jats:p>\n               <jats:p>In order to show that the structure which satisfies all eleven Tarski\u2019s axioms really exists, we provided a proof of the registration of a cluster that the Euclidean plane, or rather a natural [5] extension of ordinary metric structure <jats:monospace>Euclid 2<\/jats:monospace> satisfies all these attributes.<\/jats:p>\n               <jats:p>Although the tradition of the mechanization of Tarski\u2019s geometry in Mizar is not as long as in Coq [11], first approaches to this topic were done in Mizar in 1990 [16] (even if this article started formal Hilbert axiomatization of geometry, and parallel development was rather unlikely at that time [8]). Connection with another proof assistant should be mentioned \u2013 we had some doubts about the proof of the Euclid\u2019s axiom and inspection of the proof taken from Archive of Formal Proofs of Isabelle [10] clarified things a bit. Our development allows for the future faithful mechanization of [13] and opens the possibility of automatically generated Prover9 proofs which was useful in the case of lattice theory [7].<\/jats:p>","DOI":"10.1515\/forma-2016-0012","type":"journal-article","created":{"date-parts":[[2016,12,12]],"date-time":"2016-12-12T10:01:46Z","timestamp":1481536906000},"page":"157-166","source":"Crossref","is-referenced-by-count":2,"title":["Tarski Geometry Axioms \u2013 Part II"],"prefix":"10.1515","volume":"24","author":[{"given":"Roland","family":"Coghetto","sequence":"first","affiliation":[{"name":"Rue de la Brasserie 5, 7100 La Louvi\u00e8re, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Grabowski","sequence":"additional","affiliation":[{"name":"Institute of Informatics, University of Bia\u0142ystok, Cio\u0142kowskiego 1M, 15-245 Bia\u0142ystok, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2016,12,8]]},"reference":[{"key":"2021040620313663081_j_forma-2016-0012_ref_001_w2aab2b8b1b1b7b1ab1ab1Aa","unstructured":"[1] Czes\u0142aw Byli\u0144ski. Introduction to real linear topological spaces. Formalized Mathematics, 13(1):99\u2013107, 2005."},{"key":"2021040620313663081_j_forma-2016-0012_ref_002_w2aab2b8b1b1b7b1ab1ab2Aa","unstructured":"[2] Czes\u0142aw Byli\u0144ski. Some basic properties of sets. Formalized Mathematics, 1(1):47\u201353, 1990."},{"key":"2021040620313663081_j_forma-2016-0012_ref_003_w2aab2b8b1b1b7b1ab1ab3Aa","doi-asserted-by":"crossref","unstructured":"[3] Roland Coghetto. Circumcenter, circumcircle and centroid of a triangle. Formalized Mathematics, 24(1):17\u201326, 2016. doi:10.1515\/forma-2016-0002.","DOI":"10.1515\/forma-2016-0002"},{"key":"2021040620313663081_j_forma-2016-0012_ref_004_w2aab2b8b1b1b7b1ab1ab4Aa","unstructured":"[4] Agata Darmochwa\u0142. The Euclidean space. Formalized Mathematics, 2(4):599\u2013603, 1991."},{"key":"2021040620313663081_j_forma-2016-0012_ref_005_w2aab2b8b1b1b7b1ab1ab5Aa","doi-asserted-by":"crossref","unstructured":"[5] Adam Grabowski. Efficient rough set theory merging. Fundamenta Informaticae, 135(4): 371\u2013385, 2014. doi:10.3233\/FI-2014-1129.","DOI":"10.3233\/FI-2014-1129"},{"key":"2021040620313663081_j_forma-2016-0012_ref_006_w2aab2b8b1b1b7b1ab1ab6Aa","doi-asserted-by":"crossref","unstructured":"[6] Adam Grabowski. Tarski\u2019s geometry modelled in Mizar computerized proof assistant. In Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016, Gda\u0144sk, Poland, September 11\u201314, 2016, pages 373\u2013381, 2016. doi:10.15439\/2016F290.","DOI":"10.15439\/2016F290"},{"key":"2021040620313663081_j_forma-2016-0012_ref_007_w2aab2b8b1b1b7b1ab1ab7Aa","doi-asserted-by":"crossref","unstructured":"[7] 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":"2021040620313663081_j_forma-2016-0012_ref_008_w2aab2b8b1b1b7b1ab1ab8Aa","doi-asserted-by":"crossref","unstructured":"[8] Adam Grabowski and Christoph Schwarzweller. On duplication in mathematical repositories. In Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, and Alan P. Sexton, editors, Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5\u201310, 2010. Proceedings, volume 6167 of Lecture Notes in Computer Science, pages 300\u2013314. Springer, 2010. doi:10.1007\/978-3-642-14128-7_26.","DOI":"10.1007\/978-3-642-14128-7_26"},{"key":"2021040620313663081_j_forma-2016-0012_ref_009_w2aab2b8b1b1b7b1ab1ab9Aa","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.","DOI":"10.1007\/s10817-015-9345-1"},{"key":"2021040620313663081_j_forma-2016-0012_ref_010_w2aab2b8b1b1b7b1ab1ac10Aa","unstructured":"[10] Timothy James McKenzie Makarios. A mechanical verification of the independence of Tarski\u2019s Euclidean Axiom. 2012. Master\u2019s thesis."},{"key":"2021040620313663081_j_forma-2016-0012_ref_011_w2aab2b8b1b1b7b1ab1ac11Aa","doi-asserted-by":"crossref","unstructured":"[11] Julien Narboux. Mechanical theorem proving in Tarski\u2019s geometry. In F. Botana and T. Recio, editors, Automated Deduction in Geometry, volume 4869 of Lecture Notes in Computer Science, pages 139\u2013156. Springer, 2007.","DOI":"10.1007\/978-3-540-77356-6_9"},{"key":"2021040620313663081_j_forma-2016-0012_ref_012_w2aab2b8b1b1b7b1ab1ac12Aa","doi-asserted-by":"crossref","unstructured":"[12] William Richter, Adam Grabowski, and Jesse Alama. Tarski geometry axioms. Formalized Mathematics, 22(2):167\u2013176, 2014. doi:10.2478\/forma-2014-0017.","DOI":"10.2478\/forma-2014-0017"},{"key":"2021040620313663081_j_forma-2016-0012_ref_013_w2aab2b8b1b1b7b1ab1ac13Aa","doi-asserted-by":"crossref","unstructured":"[13] Wolfram Schwabh\u00e4user, Wanda Szmielew, and Alfred Tarski. Metamathematische Methoden in der Geometrie. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1983.","DOI":"10.1007\/978-3-642-69418-9"},{"key":"2021040620313663081_j_forma-2016-0012_ref_014_w2aab2b8b1b1b7b1ab1ac14Aa","doi-asserted-by":"crossref","unstructured":"[14] Alfred Tarski and Steven Givant. Tarski\u2019s system of geometry. Bulletin of Symbolic Logic, 5(2):175\u2013214, 1999.","DOI":"10.2307\/421089"},{"key":"2021040620313663081_j_forma-2016-0012_ref_015_w2aab2b8b1b1b7b1ab1ac15Aa","unstructured":"[15] Andrzej Trybulec and Czes\u0142aw Byli\u0144ski. Some properties of real numbers. Formalized Mathematics, 1(3):445\u2013449, 1990."},{"key":"2021040620313663081_j_forma-2016-0012_ref_016_w2aab2b8b1b1b7b1ab1ac16Aa","unstructured":"[16] Wojciech A. Trybulec. Axioms of incidence. Formalized Mathematics, 1(1):205\u2013213, 1990."},{"key":"2021040620313663081_j_forma-2016-0012_ref_017_w2aab2b8b1b1b7b1ab1ac17Aa","unstructured":"[17] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291\u2013296, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/2\/article-p157.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0012","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,7]],"date-time":"2021-04-07T00:59:41Z","timestamp":1617757181000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0012"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,1]]},"references-count":17,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2016,12,8]]},"published-print":{"date-parts":[[2016,6,1]]}},"alternative-id":["10.1515\/forma-2016-0012"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0012","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2016,6,1]]}}}