{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T16:10:46Z","timestamp":1777479046102,"version":"3.51.4"},"reference-count":18,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"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":[[2023,9,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>In the article, we continue the formalization of the work devoted to Tarski\u2019s geometry \u2013 the book \u201cMetamathematische Methoden in der Geometrie\u201d by W. Schwabh\u00e4user, W. Szmielew, and A. Tarski. We use the Mizar system to formalize Chapter 9 of this book. We deal with half-planes and planes proving their properties as well as the theory of intersecting lines.<\/jats:p>","DOI":"10.2478\/forma-2023-0026","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T10:21:58Z","timestamp":1704450118000},"page":"325-339","source":"Crossref","is-referenced-by-count":1,"title":["Tarski Geometry Axioms. Part V \u2013 Half-planes and Planes"],"prefix":"10.2478","volume":"31","author":[{"given":"Roland","family":"Coghetto","sequence":"first","affiliation":[{"name":"cafr-MSA2P asbl Rue de la Brasserie 5 7100 La Louvi\u00e8re , Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Grabowski","sequence":"additional","affiliation":[{"name":"Faculty of Computer Science , University of Bia\u0142ystok , Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2023,12,31]]},"reference":[{"key":"2026042801415090414_j_forma-2023-0026_ref_001","doi-asserted-by":"crossref","unstructured":"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":"2026042801415090414_j_forma-2023-0026_ref_002","doi-asserted-by":"crossref","unstructured":"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":"2026042801415090414_j_forma-2023-0026_ref_003","doi-asserted-by":"crossref","unstructured":"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\u2013510. Springer, 2014. doi:10.1007\/978-3-319-08587-6 38.","DOI":"10.1007\/978-3-319-08587-6_38"},{"key":"2026042801415090414_j_forma-2023-0026_ref_004","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/s10817-016-9374-4"},{"key":"2026042801415090414_j_forma-2023-0026_ref_005","unstructured":"Roland Coghetto. Tarski\u2019s parallel postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid. Archive of Formal Proofs, January 2021. https:\/\/isa-afp.org\/entries\/IsaGeoCoq.html, Formal proof development."},{"key":"2026042801415090414_j_forma-2023-0026_ref_006","doi-asserted-by":"crossref","unstructured":"Roland Coghetto and Adam Grabowski. Tarski geometry axioms \u2013 Part II. Formalized Mathematics, 24(2):157\u2013166, 2016. doi:10.1515\/forma-2016-0012.","DOI":"10.1515\/forma-2016-0012"},{"key":"2026042801415090414_j_forma-2023-0026_ref_007","doi-asserted-by":"crossref","unstructured":"Roland Coghetto and Adam Grabowski. Tarski geometry axioms. Part III. Formalized Mathematics, 25(4):289\u2013313, 2017. doi:10.1515\/forma-2017-0028.","DOI":"10.1515\/forma-2017-0028"},{"key":"2026042801415090414_j_forma-2023-0026_ref_008","doi-asserted-by":"crossref","unstructured":"Roland Coghetto and Adam Grabowski. Tarski geometry axioms. Part IV \u2013 right angle. Formalized Mathematics, 27(1):75\u201385, 2019. doi:10.2478\/forma-2019-0008.","DOI":"10.2478\/forma-2019-0008"},{"key":"2026042801415090414_j_forma-2023-0026_ref_009","doi-asserted-by":"crossref","unstructured":"Sana Stojanovic Durdevic, Julien Narboux, and Predrag Jani\u010di\u0107. 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\u2013269, 2015.","DOI":"10.1007\/s10472-014-9443-5"},{"key":"2026042801415090414_j_forma-2023-0026_ref_010","doi-asserted-by":"crossref","unstructured":"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 \u2013 Annals of Computer Science and Information Systems, pages 373\u2013381, 2016. doi:10.15439\/2016F290.","DOI":"10.15439\/2016F290"},{"key":"2026042801415090414_j_forma-2023-0026_ref_011","unstructured":"Adam Grabowski and Roland Coghetto. Tarski\u2019s geometry and the Euclidean plane in Mizar. In Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bia\u0142ystok, Poland, July 25\u201329, 2016, volume 1785 of CEUR-WS, pages 4\u20139. CEURWS.org, 2016."},{"key":"2026042801415090414_j_forma-2023-0026_ref_012","unstructured":"Haragauri Narayan Gupta. Contributions to the Axiomatic Foundations of Geometry. PhD thesis, University of California-Berkeley, 1965."},{"key":"2026042801415090414_j_forma-2023-0026_ref_013","unstructured":"Timothy James McKenzie Makarios. A mechanical verification of the independence of Tarski\u2019s Euclidean Axiom. Victoria University of Wellington, New Zealand, 2012. Master\u2019s thesis."},{"key":"2026042801415090414_j_forma-2023-0026_ref_014","unstructured":"Timothy James McKenzie Makarios. The independence of Tarski\u2019s Euclidean Axiom. Archive of Formal Proofs, October 2012. Formal proof development."},{"key":"2026042801415090414_j_forma-2023-0026_ref_015","unstructured":"Timothy James McKenzie Makarios. A further simplification of Tarski\u2019s axioms of geometry. Note di Matematica, 33(2):123\u2013132, 2014."},{"key":"2026042801415090414_j_forma-2023-0026_ref_016","doi-asserted-by":"crossref","unstructured":"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":"2026042801415090414_j_forma-2023-0026_ref_017","doi-asserted-by":"crossref","unstructured":"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":"2026042801415090414_j_forma-2023-0026_ref_018","doi-asserted-by":"crossref","unstructured":"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":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2023-0026","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T14:04:41Z","timestamp":1777385081000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2023-0026"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,1]]},"references-count":18,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2023,12,31]]},"published-print":{"date-parts":[[2023,9,1]]}},"alternative-id":["10.2478\/forma-2023-0026"],"URL":"https:\/\/doi.org\/10.2478\/forma-2023-0026","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,1]]}}}