CONTEJEAN Evelyne
Doctorat
Equipe : Toccata
Éléments pour la Décidabilité de l'Unification modulo la Distributivité.
Début le 01/09/1988
Direction :
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement :
Soutenue le 03/04/1992 devant le jury composé de :
Gérard HUET, Président
Alain COLMERAUER
Mehmet DINCBAS
Marie-Claude GAUDEL
Jean-Pierre JOUANNAUD
Claude KIRCHNER
Leszec PACHOLSKI
Activités de recherche :
- Démonstration automatique
- Réécriture
Résumé :
Dans cette thèse, nous donnons des outils pour l'unification (ou résolution d'équations) modulo la distributivité (ou modulo D) d'un symbole f sur un symbole g. Cette théorie est l'une des dernières qui soit dérivée de l'arithmétique et pour laquelle il n'est toujours pas connu si l'unification est décidable ou non.
Dans une première partie, nous étudions des problèmes particuliers pour lesquels la décidabilité est triviale, les problèmes équilibrés où les termes ne comportent pas de symboles g. Nous décrivons de façon précise l'ensemble (éventuellement infini) des solutions grâce aux structures, qui possèdent une propriété de décomposition maximale unique vis-à-vis d'un opérateur AC1. Dans une deuxième partie, nous introduisons les notions d'indexation et de stratification qui permettent de donner une caractérisation de l'égalité de termes modulo D. Nous utilisons ensuite les propriétés de la stratification pour démontrer la complétude d'un ensemble de règles de transformation, qui réduisent un problème à un problème équilibré, lequel est ensuite facilement résolu grâce à un passage à un problème modulo AC1 dans les structures. Pur des raisons techniques, nous ne traitons qu'un cas particulier caractérisé par une condition d'acyclicité dans un graphe. Nous décrivons enfin un algorithme original et efficace de résolution de systèmes linéaires d'équations diophantiennes.
