Programming and certifying a CAD algorithm in the Coq system

Mahboubi, Assia

doi:10.4230/DagSemProc.05021.17

Document

Programming and certifying a CAD algorithm in the Coq system

Author Assia Mahboubi

Part of: Volume: Dagstuhl Seminar Proceedings, Volume 5021
Part of: Series: Dagstuhl Seminar Proceedings (DagSemProc)
License: Creative Commons Attribution 4.0 International license
Publication Date: 2006-01-16

PDF

File

PDF

DagSemProc.05021.17.pdf

Filesize: 379 kB
18 pages

Document Identifiers

DOI: 10.4230/DagSemProc.05021.17
URN: urn:nbn:de:0030-drops-2763

Subject Classification

Keywords

Computer algebra
Bernstein polynomials
subresultants
CAD
Coq
certification.

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get 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) https://doi.org/10.4230/DagSemProc.05021.17

Author Details

Assia Mahboubi

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail