A Synthetic Proof of Pappus’ Theorem in Tarski’s Geometry

Journal of Automated Reasoning - Tập 58 - Trang 209-230 - 2016
Gabriel Braun1, Julien Narboux1
1ICube, UMR 7357, University of Strasbourg - CNRS, Strasbourg, France

Tóm tắt

In this paper, we report on the formalization of a synthetic proof of Pappus’ theorem. We provide two versions of the theorem: the first one is proved in neutral geometry (without assuming the parallel postulate), the second (usual) version is proved in Euclidean geometry. The proof that we formalize is the one presented by Hilbert in The Foundations of Geometry, which has been described in detail by Schwabhäuser, Szmielew and Tarski in part I of Metamathematische Methoden in der Geometrie. We highlight the steps that are still missing in this later version. The proofs are checked formally using the Coq proof assistant. Our proofs are based on Tarski’s axiom system for geometry without any continuity axiom. This theorem is an important milestone toward obtaining the arithmetization of geometry, which will allow us to provide a connection between analytic and synthetic geometry.

Tài liệu tham khảo

Boutry, P., Braun, G., Narboux, J.: From Tarski to Descartes: formalization of the arithmetization of euclidean geometry. In: The 7th International Symposium on Symbolic Computation in Software (SCSS 2016), EasyChair Proceedings in Computing, p. 15. Tokyo, Japan (2016)

Beeson, M.: Proof and computation in geometry. In: Ida, T., Fleuriot, J. (eds.) Automated Deduction in Geometry (ADG 2012), Volume 7993 of Springer Lecture Notes in Artificial Intelligence, pp. 1–30. Springer, Heidelberg (2013)

Beeson, M.: A constructive version of Tarski’s geometry. Ann. Pure Appl. Log. 166(11), 1199–1273 (2015)

Behnke, H., Gould, S.H.: Fundamentals of Mathematics: Geometry. MIT Press, New York (1974)

Bezem, M., Hendriks, D.: On the mechanization of the proof of Hessenberg’s theorem in coherent logic. J. Autom. Reason. 40(1), 61–85 (2008)

Braun, G., Narboux, J.: From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds.) Post-Proceedings of Automated Deduction in Geometry 2012, Volume 7993 of LNCS, pp. 89–109. Springer, Edinburgh (2012)

Boutry, P., Narboux, J., Schreck, P.: A Reflexive Tactic for Automated Generation of Proofs of Incidence to an Affine Variety. October (2015)

Boutry, P., Narboux, J., Schreck, P.: Parallel Postulates and Decidability of Intersection of Lines: A Mechanized Study Within Tarski’s System of Geometry. Submitted, July (2015)

Boutry, P., Narboux, J., Schreck, P., Braun, G.: Ashort note about case distinctions in Tarski’s geometry. In: Botana, F., Quaresma, P. (eds.) Automated Deduction in Geometry 2014, Proceedings of ADG 2014, pp. 1–15. Coimbra, Portugal (2014)

Boutry, P., Narboux, J., Schreck, P., Braun, G.: Using small scale automation to improve both accessibility andreadability of formal proofs in geometry. In: Botana, F., Quaresma, P. (eds.) Automated Deduction in Geometry2014, Proceedings of ADG 2014, pp. 1–19. Coimbra, Portugal (2014)

Castéran, P.: Coq + \(\epsilon \)? In: JFLA, pp. 1–15 (2007)

Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-order intuitionistic formalization and proofs in Hilbert’s elementary geometry. In: Automated Deduction in Geometry (2000)

Grégoire, B., Pottier, L., Théry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: Post-Proceedings of Automated Deduction in Geometry (ADG 2008), Number 6701 in Lecture Notes in Artificial Intelligence (2011)

Hilbert, D.: Foundations of Geometry (Grundlagen der Geometrie). Open Court, La Salle, Illinois, 1960. Second English edition, translated from the tenth German edition by Leo Unger. Original publication date (1899)

Janicic, P., Narboux, J., Quaresma, P.: The area method: a recapitulation. J. Autom. Reason. 48(4), 489–532 (2012)

Magaud, N., Narboux, J., Schreck, P.: A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom. 45(8), 406–424 (2012)

Narboux, J.: Mechanical theorem proving in Tarski’s geometry. In: Botana, F., Lozano, E.R. (eds.), Post-Proceedings of Automated Deduction in Geometry 2006, Volume 4869 of LNCS, pp. 139–156. Springer, Pontevedra, Spain (2007)

Oryszczyszyn, H., Prazmowski, K.: Classical configurations in affine planes. J. Formaliz. Math. 2 (1990)

Pasch, M.: Vorlesungen über Neuere Geometrie. Springer, New York (1976)

Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs, Volume 5170 of Lecture Notes in Computer Science, pp. 278–293. Springer, New York (2008)

Schwabhäuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983)

Thông tin
Thông tin xuất bản

Journal of Automated Reasoning

Tập 58

209-230

Thông tin tác giả