From Hilbert to Tarski

Abstract : In this paper, we describe the formal proof using the Coq proof assistant that Tarski's axioms for plane neutral geometry (excluding continuity axioms) can be derived from the corresponding Hilbert's axioms. Previously, we mechanized the proof that Tarski's version of the parallel postulate is equivalent to the Playfair's postulate used by Hilbert [9] and that Hilbert's axioms for plane neutral geometry (excluding continuity) can be derived from the corresponding Tarski's axioms [12]. Hence, this work allows us to complete the formal proof of the equivalence between the two axiom systems for neutral and plane Euclidean geometry. Formalizing Hilbert's axioms is not completely straightforward, in this paper we describe the corrections we had to make to our previous formalization. We mechanized the proof of Hilbert's theorems that are required in our proof of Tarski's axioms. But this connection from Hilbert's axioms, allows to recover the many results we obtained previously in the context of Tarski's geometry: this includes the theorems of Pappus[13], Desargues, Pythagoras and the arithmetiza-tion of geometry [8].
Type de document :
Communication dans un congrès
Eleventh International Workshop on Automated Deduction in Geometry, Jun 2016, Strasbourg, France. pp.19, 2016, Proceedings of ADG 2016. 〈http://icube-web.unistra.fr/adg2016/index.php/Accueil〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01332044
Contributeur : Julien Narboux <>
Soumis le : mercredi 15 juin 2016 - 10:42:47
Dernière modification le : mercredi 24 mai 2017 - 01:02:47
Document(s) archivé(s) le : vendredi 16 septembre 2016 - 10:12:08

Fichier

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

Identifiants

  • HAL Id : hal-01332044, version 1

Collections

Citation

Gabriel Braun, Pierre Boutry, Julien Narboux. From Hilbert to Tarski. Eleventh International Workshop on Automated Deduction in Geometry, Jun 2016, Strasbourg, France. pp.19, 2016, Proceedings of ADG 2016. 〈http://icube-web.unistra.fr/adg2016/index.php/Accueil〉. 〈hal-01332044〉

Partager

Métriques

Consultations de la notice

76

Téléchargements de fichiers

221