Paper Info
Title
From Tarski to Hilbert.
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.
Year
DOI
Venue
2012
10.1007/978-3-642-40672-0_7
Lecture Notes in Artificial Intelligence
Keywords
Field
DocType
geometry,formal proof
Discrete mathematics,Axiom,Mathematical proof,Classical logic,Calculus,Mathematics,Formal proof,Proof assistant
Conference
Volume
ISSN
Citations 
7993
0302-9743
4
PageRank 
References 
Authors
0.71
12
2
Name
Order
Citations
PageRank
Gabriel Braun1101.85
Julien Narboux213012.49