Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Mahboubi, Assia License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-2763
URL:

Programming and certifying a CAD algorithm in the Coq system

pdf-format:


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:DagSemProc.05021.17,
  author =	{Mahboubi, Assia},
  title =	{{Programming and certifying a CAD algorithm in the Coq system}},
  booktitle =	{Mathematics, Algorithms, Proofs},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5021},
  editor =	{Thierry Coquand and Henri Lombardi and Marie-Fran\c{c}oise Roy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/276},
  URN =		{urn:nbn:de:0030-drops-2763},
  doi =		{10.4230/DagSemProc.05021.17},
  annote =	{Keywords: Computer algebra, Bernstein polynomials, subresultants, CAD, Coq, certification.}
}

Keywords: Computer algebra, Bernstein polynomials, subresultants, CAD, Coq, certification.
Seminar: 05021 - Mathematics, Algorithms, Proofs
Issue date: 2006
Date of publication: 16.01.2006


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI