Unification in syntactic theories
Unification dans les théories syntaxiques
Résumé
Not available
L'objectif de cette thèse est l'étude d'une sous-classe des théories équationnelles appelée classe des théories syntaxiques. Après avoir introduit les notions de base, un ensemble de règles pour l'unification par décomposition dans les théories syntaxiques est donné. Ensuite, c'est le lien entre syntaxicité et système formel de la logique équationnelle qui est développé. Par ailleurs, un lien entre unification et syntaxicité est exposé. Une conséquence de ce résultat est: une théorie est syntaxique si elle est finitaire pour l'unification. Vient alors la question de savoir si la syntaxicité est une propriété décidable. Nous montrons que ce n'est malheureusement pas le cas, et ceci même en imposant des conditions très restrictives. Un résultat du même ordre est démontre pour la validité uniforme du problème du mot dans les théories syntaxiques. Suite à ces résultats d'indécidabilité, différentes restrictions sont étudiées. Finalement, la décidabilité du filtrage et de l'unification est démontrée pour certaines sous-classes de théories syntaxiques