Tarski Geometry Axioms. Part V – Half-planes and Planes

Pole DC	Wartość	Język
dc.contributor.author	Coghetto, Roland	-
dc.contributor.author	Grabowski, Adam	-
dc.date.accessioned	2024-01-26T11:28:50Z	-
dc.date.available	2024-01-26T11:28:50Z	-
dc.date.issued	2023	-
dc.identifier.citation	Formalized Mathematics, Volume 31, Issue 1, Pages 325-339	pl
dc.identifier.issn	1426-2630	-
dc.identifier.uri	http://hdl.handle.net/11320/15866	-
dc.description.abstract	In the article, we continue the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” by W. Schwabhäuser, 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.	pl
dc.language.iso	en	pl
dc.publisher	DeGruyter Open	pl
dc.rights	Attribution-ShareAlike 3.0 Unported (CC BY-SA 3.0)	pl
dc.rights.uri	https://creativecommons.org/licenses/by-sa/3.0/	pl
dc.subject	Tarski geometry	pl
dc.subject	half-plane	pl
dc.subject	plane	pl
dc.title	Tarski Geometry Axioms. Part V – Half-planes and Planes	pl
dc.type	Article	pl
dc.rights.holder	© 2022 The Author(s)	pl
dc.rights.holder	CC BY-SA 3.0 license	pl
dc.identifier.doi	10.2478/forma-2023-0026	-
dc.description.Affiliation	Roland Coghetto - cafr-MSA2P asbl, Rue de la Brasserie 5, 7100 La Louvi`ere, Belgium	pl
dc.description.Affiliation	Adam Grabowski - Faculty of Computer Science, University of Białystok, Poland	pl
dc.description.references	Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, 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–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.	pl
dc.description.references	Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.	pl
dc.description.references	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.	pl
dc.description.references	Gabriel Braun and Julien Narboux. A synthetic proof of Pappus’ theorem in Tarski’s geometry. Journal of Automated Reasoning, 58(2):23, 2017. doi:10.1007/s10817-016-9374-4.	pl
dc.description.references	Roland Coghetto. Tarski’s 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.	pl
dc.description.references	Roland Coghetto and Adam Grabowski. Tarski geometry axioms – Part II. Formalized Mathematics, 24(2):157–166, 2016. doi:10.1515/forma-2016-0012.	pl
dc.description.references	Roland Coghetto and Adam Grabowski. Tarski geometry axioms. Part III. Formalized Mathematics, 25(4):289–313, 2017. doi:10.1515/forma-2017-0028.	pl
dc.description.references	Roland Coghetto and Adam Grabowski. Tarski geometry axioms. Part III. Formalized Mathematics, 25(4):289–313, 2017. doi:10.1515/forma-2017-0028.	pl
dc.description.references	Sana Stojanovic Durdevic, Julien Narboux, and Predrag Janiˇcić. Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry. Annals of Mathematics and Artificial Intelligence, 74(3-4):249–269, 2015.	pl
dc.description.references	Adam Grabowski. Tarski’s 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.	pl
dc.description.references	Adam Grabowski and Roland Coghetto. Tarski’s 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łystok, Poland, July 25–29, 2016, volume 1785 of CEUR-WS, pages 4–9. CEUR-WS.org, 2016.	pl
dc.description.references	Haragauri Narayan Gupta. Contributions to the Axiomatic Foundations of Geometry. PhD thesis, University of California-Berkeley, 1965.	pl
dc.description.references	Timothy James McKenzie Makarios. A mechanical verification of the independence of Tarski’s Euclidean Axiom. Victoria University of Wellington, New Zealand, 2012. Master’s thesis.	pl
dc.description.references	Timothy James McKenzie Makarios. The independence of Tarski’s Euclidean Axiom. Archive of Formal Proofs, October 2012. Formal proof development.	pl
dc.description.references	Timothy James McKenzie Makarios. A further simplification of Tarski’s axioms of geometry. Note di Matematica, 33(2):123–132, 2014.	pl
dc.description.references	Julien Narboux. Mechanical theorem proving in Tarski’s 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.	pl
dc.description.references	William Richter, Adam Grabowski, and Jesse Alama. Tarski geometry axioms. Formalized Mathematics, 22(2):167–176, 2014. doi:10.2478/forma-2014-0017.	pl
dc.description.references	Wolfram Schwabhäuser, Wanda Szmielew, and Alfred Tarski. Metamathematische Methoden in der Geometrie. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1983.	pl
dc.identifier.eissn	1898-9934	-
dc.description.volume	31	pl
dc.description.issue	1	pl
dc.description.firstpage	325	pl
dc.description.lastpage	339	pl
dc.identifier.citation2	Formalized Mathematics	pl
dc.identifier.orcid	0000-0002-4901-0766	-
dc.identifier.orcid	0000-0001-5026-3990	-
Występuje w kolekcji(ach):	Artykuły naukowe (WInf) Formalized Mathematics, 2023, Volume 31, Issue 1

Pliki w tej pozycji:

Plik	Opis	Rozmiar	Format
Tarski-Geometry-Axioms-Part-V-Halfplanes-and-Planes.pdf		291,52 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL