Mahboubi, Assia
Programming and certifying a CAD algorithm in the Coq system
Abstract
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.
BibTeX  Entry
@InProceedings{mahboubi:DSP:2006:276,
author = {Assia Mahboubi},
title = {Programming and certifying a CAD algorithm in the Coq system},
booktitle = {Mathematics, Algorithms, Proofs},
year = {2006},
editor = {Thierry Coquand and Henri Lombardi and MarieFran{\c{c}}oise Roy},
number = {05021},
series = {Dagstuhl Seminar Proceedings},
ISSN = {18624405},
publisher = {Internationales Begegnungs und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2006/276},
annote = {Keywords: Computer algebra, Bernstein polynomials, subresultants, CAD, Coq, certification.}
}
2006
Keywords: 

Computer algebra, Bernstein polynomials, subresultants, CAD, Coq, certification. 
Seminar: 

05021  Mathematics, Algorithms, Proofs

Related Scholarly Article: 


Issue date: 

2006 
Date of publication: 

2006 