Skip to Main content Skip to Navigation
Conference papers

From Tarski to Hilbert

Gabriel Braun 1, * Julien Narboux 1
* Corresponding author
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-00727117
Contributor : Julien Narboux <>
Submitted on : Friday, March 22, 2013 - 3:15:33 PM
Last modification on : Saturday, October 27, 2018 - 1:26:51 AM
Long-term archiving on: : Monday, June 24, 2013 - 12:15:14 PM

File

adg2012_braun_narboux_postproc...
Files produced by the author(s)

Identifiers

Citation

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

Share

Metrics

Record views

722

Files downloads

728