From Tarski to Hilbert

Gabriel Braun 1, * Julien Narboux 1
* Auteur correspondant
1 IGG
ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Abstract : In this paper, we report on the formal proof that Hilbert's axiom system can be derived from Tarski's system. For this purpose we mechanized the proofs of the first twelve chapters of Schwabauser, Szmielew and Tarski's book: Metamathematische Methoden in der Geometrie. The proofs are checked formally within classical logic using the Coq proof assistant. The goal of this development is to provide clear foundations for other formalizations of geometry and implementations of decision procedures.
Type de document :
Communication dans un congrès
Tetsuo Ida and Jacques Fleuriot. Automated Deduction in Geometry 2012, Sep 2012, Edinburgh, United Kingdom. Springer, 7993, pp.89-109, 2012, <10.1007/978-3-642-40672-0_7>
Liste complète des métadonnées


https://hal.inria.fr/hal-00727117
Contributeur : Julien Narboux <>
Soumis le : vendredi 22 mars 2013 - 15:15:33
Dernière modification le : vendredi 3 février 2017 - 01:01:30
Document(s) archivé(s) le : lundi 24 juin 2013 - 12:15:14

Fichier

adg2012_braun_narboux_postproc...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Gabriel Braun, Julien Narboux. From Tarski to Hilbert. Tetsuo Ida and Jacques Fleuriot. Automated Deduction in Geometry 2012, Sep 2012, Edinburgh, United Kingdom. Springer, 7993, pp.89-109, 2012, <10.1007/978-3-642-40672-0_7>. <hal-00727117v2>

Partager

Métriques

Consultations de
la notice

420

Téléchargements du document

393