Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 8

Proceedings of the 2016 Federated Conference on Computer Science and Information Systems

Tarski's geometry modelled in Mizar computerized proof assistant

DOI: http://dx.doi.org/10.15439/2016F290

Citation: Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 8, pages 373–381 ()

Full text

Abstract. In the paper, we discuss the formal approach to Tarski geometry axioms modelled with the help of the Mizar computerized proof assistant system. Although our basic development was inspired by Julien Narboux's Coq pseudo-code and is dated back to 2014, there are significant steps in the formalization of geometry done in the last decade of the previous century. Taking this into account, we will propose the reuse of existing results within this new framework (including Hilbert's axiomatic approach), with the ultimate future goal to encode the textbook \emph{Metamathematische Methoden in der Geometrie} by Schwabh\''auser, Szmielew and Tarski. We try however to go much further from the use of simple predicates in the direction of the use of structures with their inheritance, attributes as a tool of more human-friendly namespaces for axioms, and registrations of clusters to obtain more automation (with the possible use of external equational theorem provers like Otter/Prover9).

References

  1. J. Alama, M. Kohlhase, L. Mamane, A. Naumowicz, P. Rudnicki, and J. Urban: Licensing the Mizar Mathematical Library, Proceedings of Mathematical Knowledge Management 2011, Lecture Notes in Artificial Intelligence, 6824, pp. 149–163 (2011) http://dx.doi.org/10.1007/978-3-642-22673-1_11
  2. J. Avigad, E. Dean, and J. Mumma: A formal system for Euclid’s Elements, Review of Symbolic Logic, 2 pp. 700–768 (2009) http://dx.doi.org/10.1017/S1755020309990098
  3. G. Bancerek, Cz. Byliński, A. Grabowski, A. Korniłowicz, R. Matuszewski, A. Naumowicz, K. Pąk, and J. Urban: Mizar: state-of-the-art and beyond, Intelligent Computer Mathematics, Lecture Notes in Computer Science 9150, pp. 261–279 (2015) http://dx.doi.org/10.1007/978-3-319-20615-8_17
  4. M. Beeson: Mixing computations and proofs, Journal of Formalized Reasoning, 9(1), pp. 71–99 (2016) http://dx.doi.org/10.6092/issn.1972-5787/4552
  5. M. Beeson and L. Wos: OTTER proofs in Tarskian geometry, in Proceedings of IJCAR 2014, Lecture Notes in Computer Science, 8562, pp. 495–510 (2014) http://dx.doi.org/10.1007/978-3-319-08587-6_38
  6. K. Borsuk and W. Szmielew: Foundations of Geometry, North-Holland (1960)
  7. G. Braun and J. Narboux: From Tarski to Hilbert, in Automated Deduction in Geometry, T. Ida and J. Fleuriot (eds.) Proceedings of ADG 2012 (2012) http://dx.doi.org/10.1007/978-3-642-40672-0_7
  8. R. Coghetto: Morley trisector theorem, Formalized Mathematics, 23(2), pp. 75–79 (2015) http://dx.doi.org/10.1515/forma-2015-0007
  9. R. Coghetto and A. Grabowski: Tarski geometry axioms – part II, Formalized Mathematics, 24(2) (2016). http://dx.doi.org/10.1515/forma-2016-0012.
  10. Y. Futa, H. Okazaki, D. Mizushima, and Y. Shidama: Operations of points on elliptic curve in projective coordinates, Formalized Mathematics, 20(1), 87–95 (2012) http://dx.doi.org/10.2478/v10037-012-0012-2
  11. A. Grabowski: Automated discovery of properties of rough sets, Fundamenta Informaticae, 128(1–2), pp. 65–79 (2013) http://dx.doi.org/10.3233/FI-2013-933
  12. A. Grabowski: Efficient rough set theory merging, Fundamenta Informaticae, 135(4), pp. 371–385 (2014) http://dx.doi.org/10.3233/FI-2014-1129
  13. A. Grabowski: Mechanizing complemented lattices within Mizar type system, Journal of Automated Reasoning, 55(3), pp. 211–221 (2015) http://dx.doi.org/10.1007/s10817-015-9333-5
  14. A. Grabowski: On the computer-assisted reasoning about rough sets, in Monitoring, Security and Rescue Techniques in Multiagent Systems, B. Dunin-Kȩplicz, A. Jankowski, M. Szczuka (Eds.), Advances in Soft Computing, 28, 215–226 (2005) http://dx.doi.org/10.1007/3-540-32370-8_15
  15. A. Grabowski: On the computer certification of fuzzy numbers, in Proceedings of 2013 Federated Conference on Computer Science and Information Systems, FedCSIS 2013, M. Ganzha, L. Maciaszek, M. Paprzycki (Eds.), pp. 51–54, IEEE (2013)
  16. A. Grabowski, A. Korniłowicz, and A. Naumowicz: Mizar in a nutshell, Journal of Formalized Reasoning, 3(2), 153–245 (2010) http://dx.doi.org/10.6092/issn.1972-5787/1980
  17. A. Grabowski and Ch. Schwarzweller: Towards automatically categorizing mathematical knowledge, In Proceedings of 2012 Federated Conference on Computer Science and Information Systems, FedCSIS 2015, M. Ganzha, L. Maciaszek, M. Paprzycki (Eds.), IEEE, 63–68 (2012)
  18. A. Grabowski, A. Korniłowicz, and Ch. Schwarzweller: Equality in computer proof-assistants, in Proceedings of 2015 Federated Conference on Computer Science and Information Systems, FedCSIS 2015, M. Ganzha, L. Maciaszek, M. Paprzycki (Eds.), IEEE, 45–54 (2015) http://dx.doi.org/10.15439/2015F229
  19. A. Grabowski and Ch. Schwarzweller: Revisions as an essential tool to maintain mathematical repositories, 14th Symposium on Towards Mechanized Mathematical Assistants, Calculemus’07/MKM’07, Lecture Notes in Computer Science, 235–249 (2007) http://dx.doi.org/10.1007/978-3-540-73086-6_20
  20. H.N. Gupta: Contributions to the axiomatic foundations of geometry, PhD thesis, University of California, Berkeley (1965)
  21. D. Hilbert: The Foundations of Geometry, Chicago: Open Court, 2nd ed. (1980)
  22. S. Kanas, A. Lecko, and M. Startek: Metric spaces, Formalized Mathematics, 1(3), pp. 607–610 (1990)
  23. A. Korniłowicz: Jordan curve theorem, Formalized Mathematics, 13(4), pp. 481–491 (2005)
  24. A. Korniłowicz: Definitional expansions in Mizar, Journal of Automated Reasoning, 55(3), pp. 257–268 (2015) http://dx.doi.org/10.1007/s10817-015-9331-7
  25. A. Korniłowicz: On rewriting rules in Mizar, Journal of Automated Reasoning, 50(2), 203–210 (2013) http://dx.doi.org/10.1007/s10817-012-9261-6
  26. Library Committee of the Association of Mizar Users, Preliminaries to structures, Mizar Mathematical Library, MML Id: STRUCT_0 (1995)
  27. M. Lombard and R. Vesley: A common axiom set for classical and intuitionistic plane geometry, Annals of Pure and Applied Logic, 95, pp. 229–255 (1998)
  28. T. Makarios: A mechanical verification of the independence of Tarski’s Euclidean Axiom, MSc thesis (2012)
  29. R. Matuszewski and P. Rudnicki: Mizar: the first 30 years, Mechanized Mathematics and Its Applications, 4(1), pp. 3–24 (2005)
  30. W. McCune: Prover9 and Mace4. Available at http://www.cs.unm.edu/~mccune/prover9/, 2005–2010.
  31. L. Meikle and J. Fleuriot: Formalizing Hilbert’s Grundlagen in Isabelle/Isar, in Proceedings of TPHOLs’03, Lecture Notes in Computer Science, 2758, pp. 319–334 (2003) http://dx.doi.org/10.1007/10930755_21
  32. K. Nakasho and Y. Shidama: Documentation generator focusing on symbols for the HTML-ized Mizar library, Proceedings of the Conference on Intelligent Computer Mathematics, CICM 2015, Lecture Notes in Computer Science, 9150, pp. 343–347 (2015) http://dx.doi.org/10.1007/978-3-319-20615-8_25
  33. J. Narboux: Mechanical theorem proving in Tarski’s geometry, in Automated Deduction in Geometry, F. Botana and T. Recio (eds.), Lecture Notes in Computer Science, 4869, pp. 139–156 (2007) http://dx.doi.org/10.1007/978-3-540-77356-6_9
  34. A. Naumowicz and A. Korniłowicz: A brief overview of Mizar, in Theorem Proving in Higher Order Logics 2009, S. Berghofer, T. Nipkow, Ch. Urban, M. Wenzel (Eds.), Lecture Notes in Computer Science, 5674, 67–72 (2009) http://dx.doi.org/10.1007/978-3-642-03359-9_5
  35. K. Pąk: Methods of lemma extraction in natural deduction proofs, Journal of Automated Reasoning, 50(2), 217–228 (2013) http://dx.doi.org/10.1007/s10817-012-9267-0
  36. A. Quaife: Automated development of Tarski’s geometry, Journal of Automated Resoning, 5(1), pp. 97–118 (1989)
  37. W. Richter: Hilbert Axiom Geometry in HOL Light, http://github.com/jrh13/hol-light/tree/master/RichterHilbertAxiomGeometry/
  38. W. Richter, A. Grabowski, and J. Alama: Tarski geometry axioms, Formalized Mathematics, 22(2), pp. 167–176 (2014) http://dx.doi.org/10.2478/forma-2014-0017
  39. P. Rudnicki and A. Trybulec: On the integrity of a repository of formalized mathematics, in Proceedings of Mathematical Knowledge Management 2003, A. Asperti, B. Buchberger, O. Caprotti (eds.) Lecture Notes in Computer Science, 2594, pp. 162–174 (2003) http://dx.doi.org/10.1007/3-540-36469-2_13
  40. W. Schwabhäuser, W. Szmielew, and A. Tarski: Metamathematische Methoden in der Geometrie, Springer-Verlag (1983)
  41. B. Shminke: Routh’s, Menelaus’ and Generalized Ceva’s Theorems, Formalized Mathematics, 20(2), pp. 157–159 (2012) http://dx.doi.org/10.2478/v10037-012-0018-9
  42. L. W. Szczerba: Tarski and geometry, Journal of Symbolic Logic, 51, pp. 907–912 (1986)
  43. A. Tarski: What is elementary geometry?, in Studies in Logic and the Foundations of Mathematics, North-Holland, pp. 16–29 (1959)
  44. A. Tarski and S. Givant: Tarski’s system of geometry, The Bulletin of Symbolic Logic, 5(2), pp. 175–214 (1999)
  45. W. A. Trybulec: Axioms of incidence, Formalized Mathematics, 1(1), pp. 205–213 (1990)
  46. J. Urban and G. Sutcliffe: Automated reasoning and presentation support for formalizing mathematics in Mizar, Lecture Notes in Computer Science, 6167, Springer, 132–146 (2010) http://dx.doi.org/10.1007/978-3-642-14128-7_12
  47. F. Wiedijk: A synthesis of the procedural and declarative styles of interactive theorem proving, Logical Methods in Computer Science, 8(1):30 (2012) http://dx.doi.org/10.2168/LMCS-8(1:30)2012
  48. F. Wiedijk: Formal proof—getting started, Notices of the American Mathematical Society, 55(11), 1408–1414 (2008)