a1 INRIA Sophia Antipolis, 2004, routes des Lucioles – B.P. 93, 06902 Sophia Antipolis Cedex, France Email: firstname.lastname@example.org
The Coq system is a Curry–Howard based proof assistant. Therefore, it contains a full functional, strongly typed programming language, which can be used to enhance the system with powerful automation tools through the implementation of reflexive tactics. We present the implementation of a cylindrical algebraic decomposition algorithm within the Coq system, whose certification leads to a proof producing decision procedure for the first-order theory of real numbers.
(Received December 01 2005)
(Revised June 29 2006)