Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 2/2017

29.04.2016

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

verfasst von: Gabriel Braun, Julien Narboux

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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.
Nächster Artikel Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
3
Note that we do not use the same notation as in the book [21].
 
4
This definition is called R in [21]. We call it Per because we want to keep single letter notations for points.
 
5
Note, however that for arithmetization of geometry we will need to use this axiom to obtain the standard axioms of an ordered field expressed using functions instead of relations [1].
 
Literatur
1.
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)
2.
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)
3.
4.
Behnke, H., Gould, S.H.: Fundamentals of Mathematics: Geometry. MIT Press, New York (1974)
5.
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)MathSciNetCrossRefMATH
6.
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)
7.
Boutry, P., Narboux, J., Schreck, P.: A Reflexive Tactic for Automated Generation of Proofs of Incidence to an Affine Variety. October (2015)
8.
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)
9.
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)
10.
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)
11.
Castéran, P.: Coq + \(\epsilon \)? In: JFLA, pp. 1–15 (2007)
12.
Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-order intuitionistic formalization and proofs in Hilbert’s elementary geometry. In: Automated Deduction in Geometry (2000)
13.
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)
14.
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)
15.
16.
Magaud, N., Narboux, J., Schreck, P.: A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom. 45(8), 406–424 (2012)MathSciNetCrossRefMATH
17.
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)
18.
Oryszczyszyn, H., Prazmowski, K.: Classical configurations in affine planes. J. Formaliz. Math. 2 (1990)
19.
20.
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)
21.
Schwabhäuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983)CrossRefMATH
Metadaten
Titel
A Synthetic Proof of Pappus’ Theorem in Tarski’s Geometry
verfasst von
Gabriel Braun
Julien Narboux
Publikationsdatum
29.04.2016
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 2/2017
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-016-9374-4

Premium Partner

    Bildnachweise