M. Boespflug, M. Dénès, and B. Grégoire, Full Reduction at Full Throttle, First International Conference on Certified Programs and Proofs CPP 2011, 2011.
DOI : 10.1007/3-540-44464-5_13
URL : https://hal.archives-ouvertes.fr/hal-00650940

C. Shang, X. Chou, and . Gao, Ritt-Wu's Decomposition Algorithm and Geometry Theorem Proving, Lecture Notes in Computer Science, vol.449, pp.207-220, 1990.

C. Shang, X. Chou, and . Gao, A class of geometry statements of constructive type and geometry theorem proving, Proceeding of CADE 92, 1992.

C. Shang, X. Chou, J. Gao, and . Zhang, Machine Proofs in Geometry, World Scientific, 1994.

C. Shang and . Chou, Mechanical Geometry Theorem Proving, 1988.

A. Chaieb and M. Wenzel, Context Aware Calculation and Deduction, Calculemus/MKM, pp.27-39, 2007.
DOI : 10.1007/978-3-540-73086-6_3

L. Fuchs, L. Gao, and S. Chou, A Formalisation of Grassmann-Cayley Algebra in Coq Geometry expert, software package Solving geometric constraint systems. I. A global propagation approach, Post-proceedings of Automated Deduction in Geometry, pp.47-54, 1998.

X. Gao and S. Chou, Solving geometric constraint systems. II. A symbolic approach and decision of Rc-constructibility, Computer-Aided Design, vol.30, issue.2, pp.115-122, 1998.
DOI : 10.1016/S0010-4485(97)00055-9

. Xian-shan, Q. Gao, and . Lin, MMP/Geometer -a software package for automated geometry reasoning, Proceedings of Automated Deduction in Geometry, pp.44-46, 2002.

B. Grégoire and A. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, Theorem Proving in Higher Order Logics, pp.98-113, 2005.
DOI : 10.1007/11541868_7

B. Grégoire, L. Pottier, and L. Théry, Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving, Post-proceedings of Automated Deduction in Geometry number 6701 in Lecture Notes in Artificial Intelligence, 2008.
DOI : 10.1007/978-3-642-21046-4_3

J. Harrison, Automating elementary number-theoretic proofs using gröbner bases, Proceedings of the 21st International Conference on Automated Deduction, pp.51-66, 2007.

J. Harrison, Without Loss of Generality, Lecture Notes in Computer Science, vol.2, issue.1892-3, pp.43-59, 2009.
DOI : 10.1007/11541868_8

P. Jani?i´jani?i´c, J. Narboux, and P. Quaresma, The Area Method: a Recapitulation, Journal of Automated Reasoning, 2010.

P. Jani?i´jani?i´c and P. Quaresma, System Description: GCLCprover + GeoThms, Automated Reasoning, pp.145-150, 2006.

D. Kapur, Geometry theorem proving using Hilbert's Nullstellensatz, Proceedings of the fifth ACM symposium on Symbolic and algebraic computation , SYMSAC '86, pp.202-208, 1986.
DOI : 10.1145/32439.32479

A. Mahboubi, ContributionsàContributions`Contributionsà la certification des calculs dans R : théorie, preuves, programmation, 2006.

J. Narboux, A Decision Procedure for Geometry in Coq, Proceedings of TPHOLs'2004, 2004.
DOI : 10.1007/978-3-540-30142-4_17
URL : https://hal.archives-ouvertes.fr/inria-00001035

J. Narboux, A Graphical User Interface for Formal Proofs in Geometry, Journal of Automated Reasoning, vol.17, issue.2, pp.161-180, 2007.
DOI : 10.1007/s10817-007-9071-4
URL : https://hal.archives-ouvertes.fr/inria-00118903

T. M. Pham, Y. Bertot, and J. Narboux, A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry, Proceedings of the 11th International Conference on Computational Science and Its Applications Lecture Notes in Computer Science, 2011.
DOI : 10.1007/978-3-642-21898-9_32
URL : https://hal.archives-ouvertes.fr/inria-00584918

M. Tuan and . Pham, An Additional Tool About the Orientation for Theorem Proving in the Coq Proof Assitant, Proceedings of Automated Deduction in Geometry, 2010.

L. Pottier, Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics, Knowledge Exchange: Automated Provers and Proof Assistants, CEUR Workshop Proceedings, p.418, 2008.

J. Robu, Geometry Theorem Proving in the Frame of the Theorema Project, 2002.

D. Wang, A new theorem discovered by computer prover, Journal of Geometry, vol.7, issue.1-2, pp.173-182, 1989.
DOI : 10.1007/BF01231031

D. Wang, GEOTHER 1.1: Handling and Proving Geometric Theorems Automatically, Proceedings of Automated Deduction in Geometry, pp.194-215, 2002.
DOI : 10.1007/978-3-540-24616-9_12
URL : https://hal.archives-ouvertes.fr/inria-00107637

W. Wu, ON THE DECISION PROBLEM AND THE MECHANIZATION OF THEOREM-PROVING IN ELEMENTARY GEOMETRY, Scientia Sinica, pp.157-179, 1978.
DOI : 10.1142/9789812791085_0008

Z. Ye, S. Chou, and X. Gao, An Introduction to Java Geometry Expert, Post-proceedings of Automated Deduction in Geometry, pp.189-195, 2008.
DOI : 10.1007/978-3-642-21046-4_10