L'objectif de ce travail était d'une part de développer des méthodes numériques permettant d'estimer de manière satisfaisante les moments résultant, agoniste et antagoniste développés autour d'une articulation et, d'autre part, d'appliquer ces méthodes à l'analyse de la coordination pluri-articulaire d'un mouvement de piétinement. Le problème de la dynamique inverse est résolu à l'aide d'une méthode d'optimisation statique des accélérations qui permet d'estimer les moments résultants en accord avec toutes les mesures cinématiques et dynamiques, tout en respectant les conditions d'équilibre mécanique de chaque segment. Les moments musculaires agoniste et antagoniste sont estimés en conditions dynamiques à l'aide d'une méthode qui comprend une étape de calibration isométrique et une procédure d'optimisation numérique qui utilise les données cinématiques, dynamiques et électromyographiques en entrée. Le modèle tient compte du comportement mécanique des muscles et de leur fonction anatomique pour obtenir une estimation physiologiquement réaliste des moments et un indice de co-contraction fiable a chaque instant du mouvement. Ces modèles sont appliqués à l'étude de la coordination pluri-articulaire d'un mouvement de piétinement, perturbé par le port d'un système élastique à l'articulation du genou. La redondance du système musculo-squelettique permet de gérer localement la perturbation en accroissant la participation des muscles extenseurs au contrôle de la cinématique du genou. Cette stratégie permet de conserver la même cinématique du mouvement et ainsi préserve l'équilibre dynamique du piétinement.

On étudie la notion de trace et les problèmes d'Abel-inverse à<br />l'aide du calcul résiduel dans les cadres projectifs et toriques.<br />Dans la première partie, on obtient une caractérisation algébrique des formes traces sur une hypersurface analytique à l'aide du calcul résiduel élémentaire d'une variable. En conséquence, une version plus forte du théorème d'Abel-inverse de Henkin et Passare est prouvée. On montre que ce théorème est conséquence de la rigidité d'un système différentiel particulier lié à une équation de type ”onde de choc” et on établit le lien avec le théorème de Wood sur l'algébricité d'une famille de germes d'hypersurfaces analytiques. Enfin, on obtient une nouvelle méthode pour calculer la dimension de l'espace des formes abéliennes de degré maximal sur une hypersurface projective.<br />Dans la seconde partie, on caractérise de manière combinatoire les familles de fibrés en droites permettant de définir une notion intrinsèque de concavité dans une variété torique complète lisse et on étudie les ensembles analytiques dégénérés correspondants. On étend ainsi la notion de trace au cas torique. Courants résidus, résidus toriques et résultants donnent une borne optimale sur le degrés des traces en les différents paramètres. Si la variété torique est projective, on obtient finalement une version torique des théorèmes de Wood et d'Abel-inverse, permettant une description plus précise du support du polynôme construit dans le cas hypersurface.

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.

La majorité des courbes et surfaces rencontrées dans la modélisation géométrique sont définies comme l'ensemble des solutions d'un système d'équations et d'inéquations algébriques (ensemble semi-algébrique). De nombreux problèmes dans différentes disciplines scientifiques font appel à des requètes de proximité telles que la recherche du ou des voisins les plus proches ou la quantification du voisinage de deux objets.<br /><br />Le diagramme de Voronoï d'un ensemble d'objets est une décomposition de l'espace en zones de proximité. La zone de proximité d'un objet est l'ensemble des points plus proches de cet objet que de tout autre objet. Les diagrammes de Voronoï permettent de répondre aux requètes de proximité après avoir identifié la zone de proximité à laquelle le point objet de la requète appartient. Le graphe dual du diagramme de Voronoï est appelé le graphe de Delaunay. Seules les approximations par des coniques peuvent garantir un ordre de continuité approprié au niveau des points de contact, ce qui est nécessaire pour garantir l'exactitude du graphe de Delaunay.<br /><br />L'objectif théorique de cette thèse est la mise en évidence des propriétés algébriques et géométriques élémentaires de la courbe déplacée d'une courbe algébrique et de réduire le calcul semi-algébrique du graphe de Delaunay à des calculs de valeurs propres. L'objectif pratique de cette thèse est le calcul certifié du graphe de Delaunay pour des ensembles semi-algébriques de faible degré dans le plan euclidien.<br /><br />La méthodologie associe l'analyse par intervalles et la géométrie algébrique algorithmique. L'idée centrale de cette thèse est qu'un pré-traitement symbolique unique peut accélérer l'évaluation numérique certifiée du détecteur de conflits dans le graphe de Delaunay. Le pré-traitement symbolique est le calcul de l'équation implicite de la courbe déplacée généralisée d'une conique. La réduction du problème semi-algébrique de la détection de conflits dans le graphe de Delaunay à un problème d'algèbre linéaire a été possible grâce à la considération du sommet de Voronoï généralisé (un concept introduit dans cette thèse).<br /><br />Le calcul numérique certifié du graphe de Delaunay a été éffectué avec une librairie de résolution de systèmes zéro-dimensionnels d'équations et d'inéquations algébriques basée sur l'analyse d'intervalles (ALIAS). Le calcul certifié du graphe de Delaunay repose sur des théorèmes sur l'unicité de racines dans des intervalles donnés (Kantorovitch et Moore-Krawczyk). Pour les coniques, les calculs sont accélérés lorsque l'on ne considère que les équations implicites des courbes déplacées.

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.