Programming and certifying the CAD algorithm inside the Coq system
Assia Mahboubi, Inria Sophia Antipolis, Sophia Antipolis Cedex · 2006
Abstract. A. Tarski has shown in 1975 that one can perform quantifier elimination in the theory of real closed fields. The introduction of the Cylindrical Algebraic Decomposition (CAD) method has later allowed to design rather feasible algorithms. Our aim is to program a reflectional decision procedure for the Coq system, using the CAD, to decide whether a (possibly multivariate) system of polynomial inequalities with rational coefficients has a solution or not. We have therefore implemented in Coq various computer algebra tools like gcd computations, subresultant polynomial or Bernstein polynomials.