Le logiciel Coq est un assistant à la preuve basé sur le Calcul des<br />Constructions Inductives.<br /> Dans cette thèse nous proposons d'améliorer l'automatisation de ce<br /> système en le dotant d'une procédure de décision réflexive et complète<br />pour la théorie du premier ordre de l'arithmétique réelle.<br /> La théorie des types implémentée par le système Coq comprend un<br />langage fonctionnel typé dans lequel nous avons programmé un<br />algorithme de Décomposition Algébrique Cylindrique (CAD). Cet<br />algorithme calcule une partition de l'espace en cellules<br />semi-algébriques sur lesquelles tous les polynômes d'une famille donnée <br />ont un signe constant et permet ainsi de décider les formules de cette théorie.<br /> Il s'agit ensuite de prouver la correction de l'algorithme et de la<br />procédure de décision associée avec l'assistant à la preuve Coq.<br /> Ce travail comprend en particulier une librairie d'arithmétique polynomiale<br />certifiée et une partie significative de la preuve formelle de correction de<br />l'algorithme des sous-résultants. Ce dernier algorithme permet de calculer<br />efficacement le plus grand commun diviseur de polynômes à coefficients dans un<br />anneau, en particulier à plusieurs variables.<br /> Nous proposons également une tactique réflexive de décision des égalités dans les<br />structures d'anneau et de semi-anneaux qui améliore les performances de l'outil<br />déjà disponible et augmente son spectre d'action en exploitant les possibilités de<br />calcul du système.<br /> Dans une dernière partie, nous étudions le contenu calculatoire d'une preuve<br />constructive d'un lemme élémentaire d'analyse réelle, le principe d'induction<br />ouverte.

Ce travail relève du registre de l'algorithmique de courbes et surfaces algébriques réelles. Dans le domaine de la représentation de formes, nous avons développé trois algorithmes. Le premier est un algorithme symbolique-numérique certifié, fortement basé sur les propriétés des polynômes sous-résultants, et permettant le calcul de la topologie d'une courbe algébrique plane avec la meilleur complexité connue. Le deuxième algorithme traite le problème du calcul de la topologie d'une courbe algébrique spatiale définie comme intersection de deux surfaces implicites. Pour construire cet algorithme, nous introduisons la notion de courbe spatiale en position pseudo-générique par rapport à un plan. Cette approche conduit à un algorithme symbolique- numérique certifié disposant de la meilleur complexité connue. Le troisième est un algorithme de maillages de surfaces implicites. C'est le premier algorithme certifié et implémenté qui traite le problème du maillage isotopique de surfaces implicites singulières. Enfin dans un travail sur les arrangements de quadriques nous fournissons un algorithme permettant de calculer un tel arrangement.