TESTS DE SATISFIABILITE DANS UN LANGAGE DE PROGRAMMATION EN LOGIQUE AVEC CONTRAINTES ENSEMBLISTES / EMMANUEL LEGROS ; SOUS LA DIRECTION DE GUY-RENE PERRIN

Date :

Editeur / Publisher : [S.l.] : [s.n.] , 1993

Format : 200 P.

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Perrin, Guy-René (Directeur de thèse / thesis advisor)

Université de Franche-Comté (1971-....) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : CE TRAVAIL PORTE SUR L'INTEGRATION DES CONTRAINTES SYMBOLIQUES SUR DES ENSEMBLES HEREDITAIREMENT FINIS DANS LES LANGAGES DE PROGRAMMATION EN LOGIQUE, CONFORMEMENT AU MODELE CLP (CONSTRAINT LOGIC PROGRAMMING). NOUS DEFINISSONS DANS CETTE THESE LA STRUCTURE D'UN LANGAGE DE PROGRAMMATION EN LOGIQUE AVEC CONTRAINTES SUR DES ENSEMBLES HEREDITAIREMENT FINIS (CLPS), DISPOSANT DES OPERATEURS D'EGALITE, D'APPARTENANCE, DE NON-APPARTENANCE, D'INCLUSION ET ENFIN, D'UNION ET D'INTERSECTION. NOUS MONTRONS QUE LE MODELE STANDARD DE LA PROGRAMMATION EN LOGIQUE (UNIFICATION DANS L'UNIVERS DE HERBRAND) EST INADAPTE EN RAISON DU CARACTERE NP-COMPLET DE L'UNIFICATION ENSEMBLISTE. NOUS PROPOSONS AU TRAVERS DE CLPS UNE APPROCHE DIFFERENTE FONDEE NON PLUS SUR L'UNIFICATION, MAIS SUR LE CONTROLE DE CONSISTANCE DES CONTRAINTES. LE PROTOTYPE CLPS A ENTIEREMENT ETE DEVELOPPE EN PROLOG. IL IMPLANTE D'UNE PART DES ALGORITHMES DE CONSISTANCE PARTIELLE SPECIFIQUE AUX CONTRAINTES ENSEMBLISTES, D'AUTRE PART DES ALGORITHMES D'ENUMERATION DES VALEURS CAPABLES DE RESOUDRE LES CONTRAINTES ENSEMBLISTES. DANS CE CONTEXTE, L'UNIFICATION ENSEMBLISTE EST VUE COMME UNE CONTRAINTE D'EGALITE, QUI A LA MANIERE DES AUTRES CONTRAINTES ENSEMBLISTES, EST RETARDEE TANT QU'IL N'EST PAS POSSIBLE DE LA RESOUDRE DE MANIERE DETERMINISTE. NOUS UTILISONS LE LANGAGE CLPS POUR RESOUDRE UN PROBLEME INDUSTRIEL DE GENIE LOGICIEL (BANC DE VALIDATION)