Formalization of Tarski's geometry in the Coq proof assistant.


Julien Narboux

In the early 60s, Wanda Szmielew and Alfred Tarski started the project of a treaty about the foundations of geometry. A systematic development of euclidean geometry based on Tarski's axioms was supposed to constitute the first part, but the early death of Wanda Szmielew  put an end to this project. Finally, Wolfram Schwabhäuser continued the project of Wanda Szmielew and Alfred Tarski. He published the treaty in 1983 in German : Metamathematische Methoden in der Geometrie.

We present here the formalization within the Coq proof assistant of the first height chapters of this book.

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