Abstract FR:

L'objectif de cette these est d'ameliorer la terminaison de l'unification semantique afin d'augmenter la declarativite des implantations des langages logico-equationnels. L'unification semantique etant indecidable, il est impossible de resoudre ce probleme de maniere definitive. Par consequent, dans cette these, nous avons etudie la terminaison de l'unification semantique sous deux aspects : l'un pratique en proposant une procedure d'e-unification dont le but est d'eviter les calculs inutiles, l'autre plus theorique en cherchant les restrictions necessaires pour toujours terminer. La premiere contribution de cette these est donc une procedure d'e-unification appelee surreduction conditionnelle dirigee par un graphe de termes. Le principe de cette procedure est d'utiliser un graphe de termes qui fait une approximation finie de l'ensemble des derivations de surreduction possibles afin d'eviter les calculs inutiles. En procedant ainsi, on peut empecher certaines boucles infinies. Nous comparons de maniere theorique la terminaison de notre procedure par rapport a d'autres algorithmes d'e-unification et nous presentons quelques resultats pratiques donnes par l'implantation de la surreduction dirigee. Dans le second volet de cette these, nous presentons des restrictions syntaxiques sur le probleme d'unification qui sont necessaires pour garantir la decidabilite de l'unifiabilite modulo un systeme de reecriture, autrement dit pour decider si le probleme d'unification que l'on resoud, a au moins une solution. Puis nous presentons un algorithme d'e-unification original base sur les langages d'arbres qui permet de decider l'unifiabilite. Cet algorithme introduit une nouvelle sorte de grammaire d'arbres qui permet de generer des langages contextuels et qui permet de representer finiment des ensembles infinis de solutions.