Résumé:
Le principe de Tarski-Seidenberg permet d'éliminer les quantificateurs dans les réels. Avec une version de ce principe due à Hörmander, présentée dans le livre <<Géométrie algébrique réelle>> de Bochnak, Coste et Roy, on a programmé en caml puis en Coq une tactique permettant de prouver des inégalités polynômiales sur les nombres réels.
On décrira dans cet exposé l'algorithme en une variable, l'implantation de la tactique, et quelques exemples.
Ce travail (en cours) est fait avec Assia Mahboubi (ENS Lyon).
The principle of Tarski-Seidenberg makes it possible to eliminate the quantifiers in real numbers. With a version of this principle due to Hörmander, presented in the book < < real algebraic Geometry > > of Bochnak, Coste and Roy, we have programmed in caml and in Coq a tactic allowing to prove polynomials inequalities on real numbers. We will describe in this talk the algorithm in one variable, the implementation of the tactic, and some examples.
This work (in progress) is made with Assia Mahboubi (ENS Lyon).
Retour au sommaire / Back to schedule