• Langue : Français
• Discipline : Informatique
• Identifiant : Inconnu
• Type de thèse : Doctorat
• Date de soutenance : 01/01/1994

Résumé en langue originale

Les contraintes ensemblistes expriment des relations entre ensembles de termes. Elles sont le plus souvent utilisees en informatique pour decrire des proprietes de programmes imperatifs logiques ou fonctionnels et conduisent a l'elaboration de procedures d'inference et de controle de type. Syntaxiquement, les contraintes ensemblistes sont des systemes d'inclusions ou de non-inclusions d'expressions construites avec des symboles de fonction et les operateurs ensemblistes classiques (union, intersection, complementaire). Les automates d'arbres peuvent etre consideres comme un puissant outil de decision. Dans cet esprit le theoreme le plus connu est sans doute celui de rabin qui obtient des resultats de decision pour un grand nombre de theories a l'aide d'automates d'arbres infinis. C'est cette demarche de resolution que nous utilisons dans cette these. Nous introduisons un nouveau type de reconnaisseurs, les automates d'ensembles d'arbres, des outils interessants a part entiere, et capables de representer par les langages qu'ils reconnaissent les solutions de systemes de contraintes ensemblistes. Nous obtenons alors un algorithme de resolution pour ces contraintes, et nous deduisons de l'etude des automates d'ensembles d'arbres des proprietes des ensembles de solutions.