M. Beeson, CONSTRUCTIVE GEOMETRY, Proceedings of the 10th Asian Logic Conference, 2010.
DOI : 10.1142/9789814293020_0002

M. Beeson, A constructive version of Tarski's geometry. Annals of Pure and Applied Logic, pp.1199-1273, 2015.

M. Beeson and L. Wos, OTTER Proofs in Tarskian Geometry, 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic Proceedings, pp.495-510, 2014.
DOI : 10.1007/978-3-319-08587-6_38

M. Beeson and L. Wos, Finding Proofs in Tarskian Geometry, Journal of Automated Reasoning, vol.16, issue.3, 2015.
DOI : 10.1007/s10817-014-9303-3

M. Beeson, Proving Hilbert's axioms in Tarski geometry, 2014.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

D. George and . Birkhoff, A set of postulates for plane geometry, based on scale and protractor, Annals of Mathematics, vol.33, pp.329-345, 1932.

P. Boutry, G. Braun, and J. Narboux, From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry, The 7th International Symposium on Symbolic Computation in Software EasyChair Proceedings in Computing, p.15, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01282550

P. Boutry, J. Narboux, and P. Schreck, Parallel postulates and decidability of intersection of lines: a mechanized study within Tarski's system of geometry. submitted, 2015.

P. Boutry, J. Narboux, and P. Schreck, A reflexive tactic for automated generation of proofs of incidence to an affine variety, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01216750

P. Boutry, J. Narboux, P. Schreck, and G. Braun, Using small scale automation to improve both accessibility and readability of formal proofs in geometry, Preliminary Proceedings of the 10th International Workshop on Automated Deduction in Geometry, pp.9-11, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00989781

G. Braun and J. Narboux, From Tarski to Hilbert, Tetsuo Ida and Jacques Fleuriot Post-proceedings of Automated Deduction in Geometry 2012, pp.89-109, 2012.
DOI : 10.1007/978-3-642-40672-0_7
URL : https://hal.archives-ouvertes.fr/hal-00727117

G. Braun and J. Narboux, A Synthetic Proof of Pappus??? Theorem in Tarski???s Geometry, Journal of Automated Reasoning, vol.45, issue.8, 2015.
DOI : 10.1007/s10817-016-9374-4

C. Dehlinger, J. Dufourd, and P. Schreck, Higher-Order Intuitionistic Formalization and Proofs in Hilbert???s Elementary Geometry, Automated Deduction in Geometry, pp.306-324, 2001.
DOI : 10.1007/3-540-45410-1_17

G. Haragauri-narayan, Contributions to the axiomatic foundations of geometry, 1965.

R. Hartshorne, Geometry : Euclid and beyond. Undergraduate texts in mathematics, 2000.

D. Hilbert, Foundations of Geometry (Grundlagen der Geometrie) Open Court, 1899.

D. Hilbert, Les fondements de la géométrie. Dunod, Paris, jacques gabay edition, 1971. Edition critique avec introduction et compléments préparée par Paul Rossier

T. J. and M. Makarios, A Mechanical Verification of the Independence of Tarski's Euclidean Axiom, 2012.

L. Meikle and J. Fleuriot, Formalizing Hilbert???s Grundlagen in Isabelle/Isar, Theorem Proving in Higher Order Logics, pp.319-334, 2003.
DOI : 10.1007/10930755_21

S. Richard, . Millman, D. George, and . Parker, Geometry, A Metric Approach with Models, 1991.

E. E. Moise, Elementary Geometry from an Advanced Standpoint, 1990.

J. Narboux, Mechanical Theorem Proving in Tarski???s Geometry, Lecture Notes in Computer Science, vol.4869, pp.139-156, 2006.
DOI : 10.1007/978-3-540-77356-6_9

W. Richter, Formalizing Rigorous Hilbert Axiomatic Geometry Proofs in the Proof Assistant Hol Light

A. Rosenthal, Vereinfachungen des Hilbertschen Systems der Kongruenzaxiome, Mathematische Annalen, vol.3, issue.2, pp.257-274, 1911.
DOI : 10.1007/BF01456653

W. Schwabhäuser, W. Szmielew, and A. Tarski, Metamathematische Methoden in der Geometrie, 1983.
DOI : 10.1007/978-3-642-69418-9

P. Scott, Mechanising Hilbert's Foundations of Geometry in Isabelle, 2008.

P. Scott and J. Fleuriot, Compass-free Navigation of Mazes, SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science, pp.143-155, 2016.

P. Scott and J. D. Fleuriot, An Investigation of Hilbert???s Implicit Reasoning through Proof Discovery in Idle-Time, Automated Deduction in Geometry -8th International Workshop, ADG 2010, pp.182-200, 2010.
DOI : 10.1007/3-540-44755-5_26

P. Scott and J. D. Fleuriot, A Combinator Language for Theorem Discovery, Intelligent Computer Mathematics -11th International Conference 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012. Proceedings, pp.371-385, 2012.
DOI : 10.1007/978-3-642-31374-5_25

A. Tarski and S. Givant, Tarski's System of Geometry. The bulletin of Symbolic Logic, pp.175-214, 1999.