{"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":1771063406701,"version":"3.50.1"},"reference-count":12,"publisher":"Walter de Gruyter GmbH","issue":"4","license":[{"start":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T00:00:00Z","timestamp":1513728000000},"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":[[2017,12,20]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p> In the article, we continue the formalization of the work devoted to Tarski\u2019s geometry - the book \u201cMetamathematische Methoden in der Geometrie\u201d by W. Schwabh\u00e4user, W. Szmielew, and A. Tarski. After we prepared some introductory formal framework in our two previous Mizar articles, we focus on the regular translation of underlying items faithfully following the abovementioned book (our encoding covers first seven chapters). Our development utilizes also other formalization efforts of the same topic, e.g. Isabelle\/HOL by Makarios, Metamath or even proof objects obtained directly from Prover9. In addition, using the native Mizar constructions (cluster registrations) the propositions (\u201cSatz\u201d) are reformulated under weaker conditions, i.e. by using fewer axioms or by proposing an alternative version that uses just another axioms (ex. Satz 2.1 or Satz 2.2).<\/jats:p>","DOI":"10.1515\/forma-2017-0028","type":"journal-article","created":{"date-parts":[[2018,3,28]],"date-time":"2018-03-28T22:16:22Z","timestamp":1522275382000},"page":"289-313","source":"Crossref","is-referenced-by-count":3,"title":["Tarski Geometry Axioms. Part III"],"prefix":"10.1515","volume":"25","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, Bia\u0142ystok , Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2018,3,28]]},"reference":[{"key":"2021040814230207810_j_forma-2017-0028_ref_001_w2aab3b7b4b1b6b1ab1ab1Aa","doi-asserted-by":"crossref","unstructured":"[1] Michael Beeson and Larry Wos. OTTER proofs in Tarskian geometry. In International Joint Conference on Automated Reasoning, volume 8562 of Lecture Notes in Computer Science, pages 495-510. Springer, 2014. doi: 10.1007\/978-3-319-08587-6 38.10.1007\/978-3-319-08587-638","DOI":"10.1007\/978-3-319-08587-6"},{"key":"2021040814230207810_j_forma-2017-0028_ref_002_w2aab3b7b4b1b6b1ab1ab2Aa","unstructured":"[2] Gabriel Braun and Julien Narboux. A synthetic proof of Pappus\u2019 theorem in Tarski\u2019s geometry. Journal of Automated Reasoning, 58(2):23, 2017. doi: 10.1007\/s10817-016-9374-4.10.1007\/s10817-016-9374-4"},{"key":"2021040814230207810_j_forma-2017-0028_ref_003_w2aab3b7b4b1b6b1ab1ab3Aa","unstructured":"[3] Roland Coghetto and Adam Grabowski. Tarski geometry axioms - Part II. Formalized Mathematics, 24(2):157-166, 2016. doi: 10.1515\/forma-2016-0012.10.1515\/forma-2016-0012"},{"key":"2021040814230207810_j_forma-2017-0028_ref_004_w2aab3b7b4b1b6b1ab1ab4Aa","unstructured":"[4] Sana Stojanovic Durdevic, Julien Narboux, and Predrag Jani\u02c7cic. Automated generation of machine verifiable and readable proofs: a case study of Tarski\u2019s geometry. Annals of Mathematics and Artificial Intelligence, 74(3-4):249-269, 2015."},{"key":"2021040814230207810_j_forma-2017-0028_ref_005_w2aab3b7b4b1b6b1ab1ab5Aa","doi-asserted-by":"crossref","unstructured":"[5] Adam Grabowski. Tarski\u2019s geometry modelled in Mizar computerized proof assistant. In Maria Ganzha, Leszek Maciaszek, and Marcin Paprzycki, editors, Proceedings of the 2016 Federated Conference on Computer Science and Information Systems (FedCSIS), volume 8 of ACSIS - Annals of Computer Science and Information Systems, pages 373-381, 2016. doi: 10.15439\/2016F290.","DOI":"10.15439\/2016F290"},{"key":"2021040814230207810_j_forma-2017-0028_ref_006_w2aab3b7b4b1b6b1ab1ab6Aa","unstructured":"[6] Haragauri Narayan Gupta. Contributions to the Axiomatic Foundations of Geometry. PhD thesis, University of California-Berkeley, 1965."},{"key":"2021040814230207810_j_forma-2017-0028_ref_007_w2aab3b7b4b1b6b1ab1ab7Aa","unstructured":"[7] Timothy James McKenzie Makarios. A mechanical verification of the independence of Tarski\u2019s Euclidean Axiom. Victoria University ofWellington, New Zealand, 2012. Master\u2019s thesis."},{"key":"2021040814230207810_j_forma-2017-0028_ref_008_w2aab3b7b4b1b6b1ab1ab8Aa","unstructured":"[8] Timothy James McKenzie Makarios. The independence of Tarski\u2019s Euclidean Axiom. Archive of Formal Proofs, October 2012. Formal proof development."},{"key":"2021040814230207810_j_forma-2017-0028_ref_009_w2aab3b7b4b1b6b1ab1ab9Aa","unstructured":"[9] Timothy James McKenzie Makarios. A further simplification of Tarski\u2019s axioms of geometry. Note di Matematica, 33(2):123-132, 2014."},{"key":"2021040814230207810_j_forma-2017-0028_ref_010_w2aab3b7b4b1b6b1ab1ac10Aa","doi-asserted-by":"crossref","unstructured":"[10] 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-156. Springer, 2007.","DOI":"10.1007\/978-3-540-77356-6_9"},{"key":"2021040814230207810_j_forma-2017-0028_ref_011_w2aab3b7b4b1b6b1ab1ac11Aa","unstructured":"[11] William Richter, Adam Grabowski, and Jesse Alama. Tarski geometry axioms. Formalized Mathematics, 22(2):167-176, 2014. doi: 10.2478\/forma-2014-0017.10.2478\/forma-2014-0017"},{"key":"2021040814230207810_j_forma-2017-0028_ref_012_w2aab3b7b4b1b6b1ab1ac12Aa","doi-asserted-by":"crossref","unstructured":"[12] 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"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/25\/4\/article-p289.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0028","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,9]],"date-time":"2021-04-09T16:35:44Z","timestamp":1617986144000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0028"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,20]]},"references-count":12,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2018,3,28]]},"published-print":{"date-parts":[[2017,12,20]]}},"alternative-id":["10.1515\/forma-2017-0028"],"URL":"https:\/\/doi.org\/10.1515\/forma-2017-0028","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2017,12,20]]}}}