Etude des symétries et de la cardinalité en calcul propositionnel : application aux algorithmes syntaxiques / Belai͏̈d Benhamou [en collaboration totale avec Sais Lakhdar] ; [sous la direction de Pierre Siegel]

Date :

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

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Intelligence artificielle

Algorithmes

Siegel, Pierre (1950-....) (Directeur de thèse / thesis advisor)

Université de Provence (1970-2011) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : DE NOMBREUX PROBLEMES INTRAITABLES AVEC LES METHODES DE RESOLUTION CLASSIQUES PRESENTENT UNE STRUCTURE TRES SYMETRIQUE (L'ECHANGE DE PROPOSITIONS LAISSE CETTE STRUCTURE INVARIANTE). DANS LA PREMIERE PARTIE, ON MONTRE QUE L'UTILISATION DES PROPRIETES DE SYMETRIES PERMET UNE AMELIORATION CONSIDERABLE DE L'EFFICACITE DES ALGORITHMES DE DEMONSTRATION AUTOMATIQUE (PREUVE DE COMPLEXITE LINEAIRE POUR LE PROBLEME DE PIGEON-HOLE, PREMIERE DEMONSTRATION AUTOMATIQUE DU PROBLEME DE RAMSEY R(3,3,3)) AINSI QU'UNE REPRESENTATION PLUS COMPACTE DE L'ENSEMBLE DES SOLUTIONS. DANS LA SECONDE PARTIE, CE TRAVAIL A AMENE LE DEVELOPPEMENT D'UNE EXPRESSION PLUS NATURELLE ET COMPACTE DES PROBLEMES, FONDEE SUR LA NOTION DE CARDINALITE QUI GENERALISE LA REPRESENTATION CLAUSALE CLASSIQUE. UNE CLAUSE GENERALISEE EST UN COUPLE (N,L): OU N DESIGNE LE NOMBRE MINIMUM DE LITTERAUX DE LA AFFECTER A VRAI. UNE METHODE DE RESOLUTION COMPLETE ET DECIDABLE POUR CES CLAUSES EST DECRITE. UNE PROPRIETE D'EQUIVALENCE ENTRE LA REPRESENTATION CLAUSALE CLASSIQUE ET CLAUSES GENERALISEES EST DEMONTRE. CETTE PROPRIETE PERMET D'ADAPTER EFFICACEMENT CERTAINS OUTILS DE LA RESOLUTION CLASSIQUE