I am interested in a textbook for studying (and teaching) foundations of geometry in the spirit of Tarski. I know that there is a rather old German book [W. Schwabhäuser, W. Szmielew, A. Tarski, Metamathematische Methoden in der Geometrie, Springer, 1983], which has not been translated to English.

On the other hand, searching through internet I found an interesting recent paper of Beeson about computer verification of Euclides "Elements" starting from Tarski's axioms. Beeson writes that in order to prove 48 theorems from the first book of Euclides, Coq generated about 200 additinal lemmas that establish some "obvious" facts, which however had to be proved rigorously. Those lemmas can compose Book 0 of "Elements", developping an infrastructure, necessary for correct development of elementary Euclidean geometry. So, I am interested if there is any textbook developing Euclidean geometry starting from 11 Tarski's axioms, which would be recommended for self-study or teaching foundations of geometry in universities.

And what about teaching elementary geometry in secondary schools? Are Tarski's axioms good for this purpose?

I am interested in a textbook for studying (and teaching) foundations of geometry in the spirit of Tarski. I know that there is a rather old German book [W. Schwabhäuser, W. Szmielew, A. Tarski, Metamathematische Methoden in der Geometrie, Springer, 1983], which has not been translated to English.

On the other hand, searching through internet I have found an interesting recent paper of Michael Beeson about computer verification of Euclides "Elements" starting from Tarski's axioms. Beeson writes that in order to prove 48 theorems from the first book of Euclides, Coq generated about 200 additinal lemmas that establish some "obvious" facts, which however had to be proved rigorously. Those lemmas can compose Book 0 of "Elements", developping an infrastructure, necessary for correct development of elementary Euclidean geometry. So, I am interested if there is any textbook developing Euclidean geometry starting from 11 Tarski's axioms, which would be recommended for self-study or teaching foundations of geometry in universities.

And what about teaching elementary geometry in secondary schools? Are Tarski's axioms good for this purpose?

I am interested in a textbook for studying (and teaching) foundations of geometry in the spirit of Tarski. I know that there is a rather old German book [W. Schwabhäuser, W. Szmielew, A. Tarski, Metamathematische Methoden in der Geometrie, Springer, 1983], which has not been translated to English.

On the other hand, searching through internet I found an interesting recent paper of Beeson about computer verification of Euclides "Elements" starting from Tarski's axioms. Beeson writes that in order to prove 48 theorems from the first book of Euclides, Coq generated about 200 additinal lemmas that establish some "obvious" facts, which however had to be proved rigorously. Those lemmas can compose Book 0 of "Elements", developping an infrastructure, necessary for correct development of elementary Euclidean geometry. So, I am interested if there is any textbook developing Euclidean geometry starting from 11 Tarski's axioms, which would be recommended for self-study or teaching foundations of geometry in universities.

And what about teaching elementary geometry in secondary schools? Are Tarski's axioms good for this purpose?

I am interested in a textbook for studying (and teaching) foundations of geometry in the spirit of Tarski. I know that there is a rather old German book [W. Schwabhäuser, W. Szmielew, A. Tarski, Metamathematische Methoden in der Geometrie, Springer, 1983], which has not been translated to English.

On the other hand, searching through internet I found an interesting recent paper of Beeson about computer verification of Euclides "Elements" starting from Tarski's axioms. Beeson writes that in order to prove 48 theorems from the first book of Euclides, Coq generated about 200 additinal lemmas that establish some "obvious" facts, which however had to be proved rigorously. Those lemmas can compose Book 0 of "Elements", developping an infrastructure, necessary for correct development of elementary Euclidean geometry. So, I am interested if there is any textbook developing Euclidean geometry starting from 11 Tarski's axioms, which would be recommended for self-study or teaching foundations of geometry in universities.

And what about teaching elementary geometry in secondary schools? Are Tarski's axioms good for this purpose?