Programming and certifying a CAD algorithm in the Coq system

Author Assia Mahboubi

Thumbnail PDF


  • Filesize: 379 kB
  • 18 pages

Document Identifiers

Author Details

Assia Mahboubi

Cite AsGet BibTex

Assia Mahboubi. Programming and certifying a CAD algorithm in the Coq system. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


A. Tarski has shown in 1948 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 various computer algebra tools like gcd computations, subresultant polynomial or Bernstein polynomials.
  • Computer algebra
  • Bernstein polynomials
  • subresultants
  • CAD
  • Coq
  • certification.


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads