A synthetic proof of Pappus' theorem in Tarski's geometry

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 detailed by Schwabhäuser , Szmielew and Tarski in part I of Metamathematische Methoden in der Geometrie. We highlight the steps which 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.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2017, 58 (2), pp.23. 〈10.1007/s10817-016-9374-4〉
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01176508
Contributeur : Julien Narboux <>
Soumis le : jeudi 31 mars 2016 - 20:57:06
Dernière modification le : jeudi 29 mars 2018 - 09:10:04

Fichier

Pappus.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas d'utilisation commerciale - Pas de modification 4.0 International License

Identifiants

Collections

Citation

Gabriel Braun, Julien Narboux. A synthetic proof of Pappus' theorem in Tarski's geometry. Journal of Automated Reasoning, Springer Verlag, 2017, 58 (2), pp.23. 〈10.1007/s10817-016-9374-4〉. 〈hal-01176508v2〉

Partager

Métriques

Consultations de la notice

284

Téléchargements de fichiers

409