Normal view MARC view ISBD view

Résolution du problème SAT et génération de modèles finis en logique du premier ordre / Gilles Audemard ; sous la direction de Belaïd Benhamou

Auteur principal : Audemard, Gilles, 1972-, AuteurAuteur secondaire : Benhamou, Belaïd, 1963-, Directeur de thèseAuteur secondaire collectivité : Université de Provence, Etablissement de soutenanceType de document : ThèseLangue : français.Pays : France.Éditeur : [S.l.] : [s.n.], 2001Description : 1 vol. (XI-138 p.) : tabl., fig. ; 30 cmBibliographie : Bibliogr. p. 131-138.Sujet MSC : 03B10, General logic, Classical first-order logic
68Q19, Theory of computing, Descriptive complexity and finite models
68Q87, Theory of computing, Probability in computer science
68T20, Computer science - Artificial intelligence, Problem solving in the context of artificial intelligence
97-02, Research exposition (monographs, survey articles) pertaining to mathematics education
Note de thèse: Thèse de doctorat, informatique, 2001, Aix-Marseille 1
Tags from this library: No tags from this library for this title. Log in to add tags.
Current location Call number Status Date due Barcode
CMI
Salle S
Thèses AUD (Browse shelf) Available 00640-01

Bibliogr. p. 131-138

Thèse de doctorat informatique 2001 Aix-Marseille 1

Dans la première partie de cette thèse nous traitons du problème SAT. Nous proposons un lagorithme permettant de détecter des mono-littéraux que la procédure de DAVIS et PUTNAM (DP) n'exploite pas. Cet algorithme est combiné avec la procédure DP créant ainsi une méthode que nous avons nommé AVAL. L'étude expérimentale que nous avons menée a mis en avant une avalanche de propagation de mono-littéraux donnant lieu à cette appellation. Dans la deuxième partie, nous abordons la génération de modèles finis pour les théories multi-types de la logique du premier ordre. Nous avons essayé d'améliorer la propagation des contraintes de diverses manières. La première utilise un pré-traitement qui modifie la syntaxe de la théorie. La deuxième est un algorithme de type "look-ahead" qui détecte les valeurs de domaines incompatibles et induit une heuristique de type UP. La dernière crée, à partir de la syntaxe de la théorie, un ordre de préférence sur les symboles fonctionnels que nous utilisons pour mettre au point des heuristiques optimisant la propagation. Les problèmes exprimés sous forme de théories multi-types contiennent souvent un grand nombre de symétries. Il est nécessaire d'en supprimer une partie pour avoir un générateur de modèles finis efficace. Certains utilisent l'heuristique LNH pour supprimer les isomorphismes triviaux. Nous proposons une extension de cette dernière, nommée XLNH , qui ne génère que les interprétations non symétriques d'une fonction unaire. Elle détecte ensuite statiquement certains isomorphismes sans sur-coût de temps. Nous avons ensuite étudié un cadre plus général de la symétrie, nous montrons de nouvelles propriétés concernant les symétries et étudions un algorithme qui permet de les détecter et de les exploiter dynamiquement. Nous montrons, notamment, que les symétries supprimées par les heuristiques LNH et XLNH sont des cas particuliers de ce cadre d'étude

There are no comments for this item.

Log in to your account to post a comment.