Using reflection to build efficient and certified decision procedures, Proceedings of TACS'97, 1997. ,
DOI : 10.1007/BFb0014565
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.7587
Machine Proofs in Geometry, World Scientific, vol.6, 1994. ,
DOI : 10.1142/2196
Mechanical Geometry Theorem Proving, 1988. ,
Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Lecture Notes In Computer Science, pp.134-183, 1975. ,
Higher-Order Intuitionistic Formalization and Proofs in Hilbert???s Elementary Geometry, Automated Deduction in Geometry, pp.306-324, 2000. ,
DOI : 10.1007/3-540-45410-1_17
Les éléments. Presses Universitaires de France, 1998. ,
Formalisation en coq d'un cours de géométrie pour le lycée, Journées Francophones des Langages Applicatifs, 2004. ,
DOI : 10.3166/tsi.24.1113-1138
Toward a " common " language for formally stating elementary geometry theorems ,
Meta theory and reflection in theorem proving:a survey and critique, 1995. ,
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 ,
Computation meta theory in nuprl, The Proceedings of the Ninth International Conference of Automated Deduction, pp.238-257, 1988. ,
Constructive geometry according to Jan von Plato. Coq contribution. Coq V5 ,
Formalizing Hilbert's grundlagen in isabelle/isar, Theorem Proving in Higher Order Logics, pp.319-334, 2003. ,
A Decision Method for Elementary Algebra and Geometry, 1951. ,
DOI : 10.1007/978-3-7091-9459-1_3
What is elementary geometry? The axiomatic Method, with special reference to Geometry and Physics, pp.16-29, 1959. ,
The axioms of constructive geometry, Annals of Pure and Applied Logic, pp.169-200, 1995. ,
ON THE DECISION PROBLEM AND THE MECHANIZATION OF THEOREM-PROVING IN ELEMENTARY GEOMETRY, Scientia Sinica, pp.157-179, 1978. ,
DOI : 10.1142/9789812791085_0008