Tarski Geometry Axioms. Part IV – Right Angle

Pole DC	Wartość	Język
dc.contributor.author	Coghetto, Roland	-
dc.contributor.author	Grabowski, Adam	-
dc.date.accessioned	2019-05-21T07:18:03Z	-
dc.date.available	2019-05-21T07:18:03Z	-
dc.date.issued	2019	-
dc.identifier.citation	Formalized Mathematics, Volume 27, Issue 1, Pages 75-85	-
dc.identifier.issn	1426-2630	-
dc.identifier.uri	http://hdl.handle.net/11320/7842	-
dc.description.abstract	In the article, we continue [7] the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” (SST for short) by W. Schwabhäuser, W. Szmielew, and A. Tarski [14], [9], [10]. We use the Mizar system to systematically formalize Chapter 8 of the SST book.We define the notion of right angle and prove some of its basic properties, a theory of intersecting lines (including orthogonality). Using the notion of perpendicular foot, we prove the existence of the midpoint (Satz 8.22), which will be used in the form of the Mizar functor (as the uniqueness can be easily shown) in Chapter 10. In the last section we give some lemmas proven by means of Otter during Tarski Formalization Project by M. Beeson (the so-called Section 8A of SST).	-
dc.language.iso	en	-
dc.publisher	DeGruyter Open	-
dc.subject	Tarski geometry	-
dc.subject	foundations of geometry	-
dc.subject	right angle	-
dc.title	Tarski Geometry Axioms. Part IV – Right Angle	-
dc.type	Article	-
dc.identifier.doi	10.2478/forma-2019-0008	-
dc.description.Affiliation	Roland Coghetto - Rue de la Brasserie 5, 7100 La Louvi`ere, Belgium	-
dc.description.Affiliation	Adam Grabowski - Institute of Informatics, University of Białystok, Poland	-
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.	-
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.	-
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.	-
dc.description.references	Michael Beeson, Julien Narboux, and Freek Wiedijk. Proof-checking Euclid. Annals of Mathematics and Artificial Intelligence, Jan 2019. doi:10.1007/s10472-018-9606-x.	-
dc.description.references	Pierre Boutry, Gabriel Braun, and Julien Narboux. Formalization of the Arithmetization of Euclidean Plane Geometry and Applications. Journal of Symbolic Computation, 90: 149–168, 2019. doi:10.1016/j.jsc.2018.04.007.	-
dc.description.references	Pierre Boutry, Charly Gries, Julien Narboux, and Pascal Schreck. Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. Journal of Automated Reasoning, 62(1):1–68, 2019.	-
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.	-
dc.description.references	Sana Stojanovic Durdevic, Julien Narboux, and Predrag Janičić. 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.	-
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.	-
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, 2016.	-
dc.description.references	Haragauri Narayan Gupta. Contributions to the Axiomatic Foundations of Geometry. PhD thesis, University of California-Berkeley, 1965.	-
dc.description.references	Julien Narboux. Mechanical theorem proving in Tarski’s geometry. In Francisco Botana and Tomas Recio, editors, Automated Deduction in Geometry, pages 139–156, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. ISBN 978-3-540-77356-6.	-
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.	-
dc.description.references	Wolfram Schwabhcuser, Wanda Szmielew, and Alfred Tarski. Metamathematische Methoden in der Geometrie. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1983.	-
dc.identifier.eissn	1898-9934	-
dc.description.volume	27	-
dc.description.issue	1	-
dc.description.firstpage	75	-
dc.description.lastpage	85	-
dc.identifier.citation2	Formalized Mathematics	-
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, 2019, Volume 27, Issue 1

Pliki w tej pozycji:

Plik	Opis	Rozmiar	Format
forma_2019_27_1_008.pdf		255,95 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki

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