Tarski Geometry Axioms. Part IV – Right Angle

[1] 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.10.1007/978-3-319-20615-8_17Open DOISearch in Google Scholar

[2] 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.10.1007/s10817-017-9440-6604425130069070Open DOISearch in Google Scholar

[3] 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-638Open DOISearch in Google Scholar

[4] 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.10.1007/s10472-018-9606-xOpen DOISearch in Google Scholar

[5] 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.10.1016/j.jsc.2018.04.007Open DOISearch in Google Scholar

[6] 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.10.1007/s10817-017-9422-8Search in Google Scholar

[7] Roland Coghetto and Adam Grabowski. Tarski geometry axioms. Part III. Formalized Mathematics, 25(4):289–313, 2017. doi:10.1515/forma-2017-0028.10.1515/forma-2017-0028Open DOISearch in Google Scholar

[8] 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.10.1007/s10472-014-9443-5Search in Google Scholar

[9] 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.10.15439/2016F290Search in Google Scholar

[10] 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.Search in Google Scholar

[11] Haragauri Narayan Gupta. Contributions to the Axiomatic Foundations of Geometry. PhD thesis, University of California-Berkeley, 1965.Search in Google Scholar

[12] 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.10.1007/978-3-540-77356-6_9Search in Google Scholar

[13] 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-0017Open DOISearch in Google Scholar

[14] Wolfram Schwabhcuser, Wanda Szmielew, and Alfred Tarski. Metamathematische Methoden in der Geometrie. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1983.10.1007/978-3-642-69418-9Search in Google Scholar