, From Hilbert to Tarski In Eleventh International Workshop on Automated Deduction in Geometry, Proceedings of ADG 2016, p.19, 2016.
, Proof and computation in geometry Automated Deduction in Geometry, Tetsuo Ida and Jacques Fleuriot, pp.1-30, 2012.
, A constructive version of Tarski's geometry, Annals of Pure and Applied Logic, vol.166, issue.11, pp.1199-1273, 2015.
DOI : 10.1016/j.apal.2015.07.006
, Hilbert's ?-operator in intuitionistic type theories, Mathematical Logic Quarterly, vol.39, issue.1, pp.323-337, 1993.
, Parallel postulates , excluded middle and continuity axioms: a mechanized study using Coq, 2017.
, Automated Theorem Proving in GeoGebra: Current Achievements, Journal of Automated Reasoning, vol.74, issue.3, pp.39-59, 2015.
DOI : 10.1007/s10817-015-9326-4
, A set of postulates for plane geometry, based on scale and protractor, Annals of Mathematics, pp.329-345, 1932.
, From Tarski to Hilbert Post-proceedings of Automated Deduction in Geometry 2012, Tetsuo Ida and Jacques Fleuriot, pp.89-109, 2012.
, A reflexive tactic for automated generation of proofs of incidence to an affine variety, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01216750
, A short note about case distinctions in Tarski's geometry, Proceedings of the 10th Int. Workshop on Automated Deduction in Geometry, volume TR 2014/01 of Proceedings of ADG 2014, pp.51-65, 2014.
, Using small scale automation to improve both accessibility and readability of formal proofs in geometry Workshop on Automated Deduction in Geometry On the unavoidable uncertainty of truth in dynamic geometry proving, Proceedings of the 10th Int, pp.31-495, 2014.
, Foundations of geometry, 1960.
, Finding Proofs in Tarskian Geometry, Journal of Automated Reasoning, vol.16, issue.3, pp.181-207, 1994.
DOI : 10.1007/s10817-014-9303-3
, Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Logical Methods in Computer Science, vol.8, issue.102, pp.1-40, 2012.
URL : https://hal.archives-ouvertes.fr/inria-00593738
, Formalization and Specification of Geometric Knowledge Objects, Automated Deduction in Geometry, volume 2061 of Lecture Notes in Computer Science, pp.439-454, 2001.
DOI : 10.1007/s11786-013-0167-4
URL : https://hal.archives-ouvertes.fr/hal-00913400
, Open Court, Chicago, 1925. first published as an appendix to the Discours de la Méthode, 1637.
, Euclid's Elements: all thirteen books complete in one volume : the Thomas L. Heath translation, 2002.
, A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry, pp.51-67, 2011.
DOI : 10.1007/978-3-7091-4368-1
URL : https://hal.archives-ouvertes.fr/hal-00657901
, Formalization of Wu???s Simple Method in Coq, CPP 2011 First International Conference on Certified Programs and Proofs, pp.71-86, 2011.
DOI : 10.1007/978-3-642-21046-4_10
, Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving number 6701 in Lecture Notes in Artificial Intelligence Mathematics for high school: Geometry. Teacher's commentary, Postproceedings of Automated Deduction in GeometryGro61] School Mathematics Study GroupGup65] Haragauri Narayan Gupta. Contributions to the axiomatic foundations of geometry, 1961.
, Open Court Second English edition, translated from the tenth German edition by Leo Unger. Original publication date, 1899. [Jan06] Predrag Jani?i´Jani?i´c. GCLC ? A Tool for Constructive Euclidean Geometry and More than That The Area Method : a Recapitulation, Proceedings of International Congress of Mathematical SoftwareJNQ12] Predrag Jani?i´Jani?i´c, pp.58-73489, 1960.
, A comparative review of recent researches in geometry, Bulletin of the American Mathematical Society, vol.2, issue.10, pp.215-249
DOI : 10.1090/S0002-9904-1893-00147-X
, Vergleichende Betrachtungen ???ber neuere geometrische Forschungen, Mathematische Annalen, vol.43, issue.1, pp.63-100, 1893.
DOI : 10.1007/BF01446615
URL : http://www.gutenberg.org/etext/38033
, Formalizing Hilbert's Grundlagen in Isabelle/Isar Elementary Geometry from an Advanced Standpoint, pp.319-334, 1990.
, Geometry: a metric approach with models, 1991.
, Formalizing complex plane geometry, Annals of Mathematics and Artificial Intelligence, vol.13, issue.2, pp.271-308, 2015.
DOI : 10.1007/s10472-014-9436-4
, Formalization and implementation of algebraic methods in geometry, Proceedings First Workshop on CTP Components for Educational Software of Electronic Proceedings in Theoretical Computer Science, pp.63-81, 2011.
, Determining automatically compass and straightedge unconstructibility in triangles, 7th International Symposium on Symbolic Computation Mar 2016. issn 2040-557X. [Nar04] Julien Narboux. A Decision Procedure for Geometry in Coq Proceedings of TPHOLs, pp.130-142, 2004.
, Mechanical Theorem Proving in Tarski's geometry Post-proceedings of Automated Deduction in Geometry, LNCS, vol.4869, pp.139-156, 2006.
, Towards A Certified Version of the Encyclopedia of Triangle Centers [Pam98] Victor Pambuccian. Zur existenz gleichseitiger dreiecke in h-ebenen Tarski geometry axioms, Mathematics in Computer Science Journal of Geometry Formalized Mathematics, vol.10, issue.222, pp.17147-153167, 1998.
, Automated Generation of Machine Verifiable and Readable Proofs: A Case Study of Tarski's Geometry, Annals of Mathematics and Artificial Intelligence, p.25, 2015.
, A new look at generalized rewriting in type theory, SST83] Wolfram Schwabhäuser, Wanda Szmielew, and Alfred Tarski. Metamathematische Methoden in der Geometrie, pp.41-62, 1983.
URL : https://hal.archives-ouvertes.fr/inria-00628904
, Tarski's system of geometry. The bulletin of Symbolic Logic Mechanical Theorem Proving in Geometries An introduction to java geometry expert, International Workshop on Automated Deduction in Geometry, pp.189-195, 1994.