Programming and certifying a CAD algorithm in the Coq system

Assia Mahboubi 1, *
* Auteur correspondant
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
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.
Type de document :
Communication dans un congrès
Dagstuhl Seminar 05021 - Mathematics, Algorithms, Proofs, Jan 2005, Dagstuhl, Germany. Dagstuhl Online Research Publication Server, 2006, 〈http://drops.dagstuhl.de/opus/volltexte/2006/276/〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00819492
Contributeur : Assia Mahboubi <>
Soumis le : mercredi 1 mai 2013 - 16:16:00
Dernière modification le : jeudi 11 janvier 2018 - 16:20:46

Identifiants

  • HAL Id : hal-00819492, version 1

Collections

Citation

Assia Mahboubi. Programming and certifying a CAD algorithm in the Coq system. Dagstuhl Seminar 05021 - Mathematics, Algorithms, Proofs, Jan 2005, Dagstuhl, Germany. Dagstuhl Online Research Publication Server, 2006, 〈http://drops.dagstuhl.de/opus/volltexte/2006/276/〉. 〈hal-00819492〉

Partager

Métriques

Consultations de la notice

53