Combinaison de résolutions de contraintes

L'objet de cette these est l'etude de la combinaison des resolutions de contraintes. La notion de contrainte a permis d'accroitre sensiblement l'efficacite des systemes de deduction a la base de la programmation en logique et de la demonstration automatique. A l'heure actuelle, les systemes de deduction incorporent le plus souvent un seul domaine de calcul qui peut etre suivant les cas, les termes du premier ordre, les entiers, les booleens, les domaines finis ou algebres finies. Le probleme de combinaison consiste a etendre l'utilisation de ces algorithmes afin qu'ils puissent resoudre des contraintes mixtes sur la reunion des domaines de calcul. Un cas particulierement important est celui de la combinaison d'algorithmes d'unification, ou les contraintes sont des equations et les domaines, des theories equationnelles a signatures disjointes. Dans cette these, nous generalisons l'emploi de techniques de combinaison aux resolutions de contraintes. Nous presentons des algorithmes d'unification dans des theories equationnelles decomposables en sous-theories non necessairement disjointes pour lesquelles des principes de combinaison sont toujours applicables. Dans la classe optimale des theories partiellement lineaires que nous introduisons, la resolution d'un probleme combine specifique comme le filtrage s'effectue par resolution de sous-problemes tout aussi specifiques. L'approche suivie permet d'appliquer la plupart de nos algorithmes de combinaison de l'unification, du filtrage ou du probleme du mot au probleme de satisfaisabilite qui revet une importance grandissante en programmation logique et en deduction automatique avec contraintes. Nous proposons un cadre formel pour la combinaison de resolveurs de contraintes symboliques. Le langage de contraintes combine et le resolveur qui en resultent sont illustres par la combinaison de resolveurs dans les algebres finies et utilises dans l'integration d'une structure predefinie au mecanisme general et incremental de resolution par surreduction contrainte.