B. Buchberger, Bruno Buchberger???s PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal, Journal of Symbolic ComputationVolume 41, Issues 3-4, Logic, Mathematics and Computer Science: Interactions in honor of Bruno Buchberger, 2006.
DOI : 10.1016/j.jsc.2005.09.007

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

D. Eisenbud, Commutative algebra with a view toward algebraic geometry, Graduate Texts in Mathematics, vol.150, 1999.

J. Faugère, A new efficient algorithm for computing Gr??bner bases (F4), issues 1-3 of Journal of Pure and Applied Algebra, pp.61-88, 1999.
DOI : 10.1016/S0022-4049(99)00005-5

J. Harrison, Towards Self-verification of HOL Light, Proceedings of the third International Joint Conference, pp.177-191, 2006.
DOI : 10.1007/11814771_17

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, Verifying Nonlinear Real Formulas Via Sums of Squares, Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, pp.102-118, 2007.
DOI : 10.1007/978-3-540-74591-4_9

L. Pottier and J. Créci, Gb: une procédure de décision pour le système coq Journées Francaises des Langages Applicatifs, Sainte-Marie-de-Ré, 2004.

L. Pottier and L. Théry, http://www-sop.inria.fr/croap/CFC/Gbcoq.html. [11] The Coq Development Team. The coq proof assistant, 1998.