Les contraintes du premier ordre offrent une grande expressivité qui permet de modéliser d'une manière très naturelle des problèmes complexes de différents domaines de l'intelligence artificielle. Mes recherches ont pour but de développer des solveurs de contraintes du premier ordre qui, pour toute formule F et un ensemble d'axiomes E, sont capables de produire une formule équivalente résolue dans E. Les problématiques qui en découlent se situent au carrefour de l'intelligence artificielle et de la vérification formelle. Je m'intéresse en particulier a la réécriture, la complétude et a la théories des arbres finis ou infinis. Tout ceci est placé dans un cadre général qui a pour buts : (1) la compréhension et l'analyse fondamentale des mécanismes de résolution afin d'aboutir a de puissants solveurs. (2) La conception de modèles performants de représentation et de calcul [plus de détail].