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.
G. Braun , J. Narboux
Post Proceedings of Automated Deduction in Geometry (ADG 2012) , Volume 7993 , page 89-109 - 2012
International conference with proceedings
From Tarski to Hilbert, Post Proceedings of Automated Deduction in Geometry (ADG 2012), Edinburgh, United Kingdom, pages 89-109, Springer, LNCS, Volume 7993, juin 2012, doi:10.1007/978-3-642-40672-0_7
Research team : IGG
Powered by Papr@Inproceedings{4-BN12,
author = {Braun, G. and Narboux, J.},
title = {From Tarski to Hilbert},
booktitle = {Post Proceedings of Automated Deduction in Geometry (ADG 2012)},
series = {LNCS},
volume = {7993},
pages = {89-109},
month = {Jun},
year = {2012},
publisher = {Springer},
doi = {10.1007/978-3-642-40672-0_7},
x-international-audience = {Yes},
x-language = {EN},
url = {http://publis.icube.unistra.fr/4-BN12}
}