We present here the formalization within the Coq proof assistant of the first 15
chapters of this book.
We also prove that Hilbert axioms can be derived from Tarski axioms (this proof does not include the continuity axioms).
Related papers:
- Julien Narboux, Mechanical Theorem Proving in Tarski's geometry, Automated Deduction in Geometry 2006, Aug 2006, Pontevedra, Spain. Springer, Automated Deduction in Geometry, 4869, pp. 139-156, 2007, LNCS, DOI : 10.1007/978-3-540-77356-6.
- Gabriel Braun and Julien Narboux, From Tarski to Hilbert, in the Post-Proceedings of ADG 2012, LNCS, 2013.
- Pierre Boutry, Julien Narboux, Pascal Schreck and Gabriel Braun, Using small scale automation to improve both accessibility and readability of formal proofs in geometry, in informal proceedings of ADG 2014.
- Pierre Boutry, Julien Narboux, Pascal Schreck and Gabriel Braun, A short note about case distinctions in Tarski's geometry, in informal proceedings of ADG 2014.
- Gabriel Braun, Julien Narboux, A synthetic proof of Pappus' theorem in Tarski's geometry, submitted to a journal, 2015.
-
- Pierre Boutry, Julien Narboux, Pascal Schreck, Parallel postulates and decidability of intersection of lines: a mechanized study within Tarski's system of geometry, submitted to a journal, 2015.
Here is an illustrated presentation
of the axioms, the main definitions and an example of a proof (in french).
Here is a .pdf file containing all the defintions and the lemmas (without proofs) .
Here is a .tgz containing all the Coq files (updated 04/2014).
You can browse the Coq files
from the index or you can have a look at one of the following chapters :
|
W. Schwabhäuser
W Szmielew
A. Tarski
Metamathematische Methoden in der Geometrie
Mit 167 Abbildungen
Teil I:Ein exiomatischer Aufbau der euklidischen Geometrie
von W.Schwabhäuser, W. Szmielew und A. Tarski
Teil II:Metamathematische Betrachtungen
von W. Schwabhäuser
Springer-Verlag 1983 |
|