Combinaison de résolutions de contraintes - Université de Lorraine Accéder directement au contenu
Thèse Année : 1993

Combination of constraint solvers

Combinaison de résolutions de contraintes

Résumé

Non disponible / Not available
L'objet de cette thèse est l'étude de la combinaison des résolutions de contraintes. La notion de contrainte a permis d'accroitre sensiblement l'efficacité des systèmes de déduction à la base de la programmation en logique et de la démonstration automatique. A l'heure actuelle, les systèmes de déduction incorporent le plus souvent un seul domaine de calcul qui peut être suivant les cas, les termes du premier ordre, les entiers, les booléens, les domaines finis ou algèbres finies. Le problème de combinaison consiste à étendre l'utilisation de ces algorithmes afin qu'ils puissent résoudre des contraintes mixtes sur la réunion des domaines de calcul. Un cas particulièrement important est celui de la combinaison d'algorithmes d'unification, ou les contraintes sont des équations et les domaines, des théories équationnelles à signatures disjointes. Dans cette thèse, nous généralisons l'emploi de techniques de combinaison aux résolutions de contraintes. Nous présentons des algorithmes d'unification dans des théories équationnelles décomposables en sous-théories non nécessairement disjointes pour lesquelles des principes de combinaison sont toujours applicables. Dans la classe optimale des théories partiellement linéaires que nous introduisons, la résolution d'un problème combiné spécifique comme le filtrage s'effectue par résolution de sous-problèmes tout aussi spécifiques. L'approche suivie permet d'appliquer la plupart de nos algorithmes de combinaison de l'unification, du filtrage ou du problème du mot au problème de satisfaisabilite qui revêt une importance grandissante en programmation logique et en déduction automatique avec contraintes. Nous proposons un cadre formel pour la combinaison de résolveurs de contraintes symboliques. Le langage de contraintes combiné et le résolveur qui en résultent sont illustrés par la combinaison de résolveurs dans les algèbres finies et utilisés dans l'intégration d'une structure prédéfinie au mécanisme général et incrémental de résolution par surréduction contrainte.
Fichier principal
Vignette du fichier
SCD_T_1993_0369_RINGEISSEN.pdf (4.5 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

tel-01747147 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01747147 , version 1

Citer

Christophe Ringeissen. Combinaison de résolutions de contraintes. Informatique [cs]. Université Henri Poincaré - Nancy 1, 1993. Français. ⟨NNT : 1993NAN10369⟩. ⟨tel-01747147⟩
68 Consultations
31 Téléchargements

Partager

Gmail Facebook X LinkedIn More