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
Context Aware Calculation and Deduction, Calculemus/MKM, pp.27-39, 2007. ,
DOI : 10.1007/978-3-540-73086-6_3
Commutative algebra with a view toward algebraic geometry, Graduate Texts in Mathematics, vol.150, 1999. ,
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
Towards Self-verification of HOL Light, Proceedings of the third International Joint Conference, pp.177-191, 2006. ,
DOI : 10.1007/11814771_17
Automating elementary number-theoretic proofs using gröbner bases, Proceedings of the 21st International Conference on Automated Deduction, pp.51-66, 2007. ,
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
Gb: une procédure de décision pour le système coq Journées Francaises des Langages Applicatifs, Sainte-Marie-de-Ré, 2004. ,
http://www-sop.inria.fr/croap/CFC/Gbcoq.html. [11] The Coq Development Team. The coq proof assistant, 1998. ,