Cette thèse traite des systèmes paramétrés. Ils modélisent des applications dans divers domaines, comme la robotique ou la calibration. Soit S un système paramétré. Nous cherchons à décrire les ouverts connexes U de l'espace des paramètres tels que S restreint à U admet un nombre constant de solutions réelles. En robotique, nous détectons les positions cuspidales des robots plan 3-RPR. En calibration photographique, nous décrivons le nombre de solutions réalisables du problème Perspective-3- Points. D'un point de vue théorique, nous montrons que sous certaines hypothèses, le calcul de la variété discriminante d'un système paramétré peut se réduire à un calcul de projection. Dans le cas des systèmes quelconques, nous introduisons la décomposition équidimensionnelle régulière. Notre algorithme possède de bonnes performances en pratique et nous permet par ailleurs de déduire un nouvel algorithme pour le calcul du radical d'un idéal.

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.