Skip to Main content Skip to Navigation
Conference papers

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].
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download
Contributor : Julien Narboux Connect in order to contact the contributor
Submitted on : Wednesday, June 15, 2016 - 10:42:47 AM
Last modification on : Wednesday, December 1, 2021 - 3:32:11 PM
Long-term archiving on: : Friday, September 16, 2016 - 10:12:08 AM


Files produced by the author(s)


  • HAL Id : hal-01332044, version 1


Gabriel Braun, Pierre Boutry, Julien Narboux. From Hilbert to Tarski. Eleventh International Workshop on Automated Deduction in Geometry, Jun 2016, Strasbourg, France. pp.19. ⟨hal-01332044⟩



Record views


Files downloads