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.