Combinaison de la propagation et de la décomposabilité pour la résolution de contraintes du premier ordre

Résumé : Les contraintes du premier ordre (toute quantification, tout symbole logique) jouent un rôle fondamental en informatique et mathématiques. D'un côté théorique la conception d'un solveur de contraintes du premier ordre dans une théorie T est la preuve formelle de la complétude de T.D'un point de vue pratique, les contraintes du premier ordre offrent une grande expressivité qui permet de modéliser d'une manière naturelle plusieurs problèmes complexes de différents domaines de l'intelligence artificielle. Un des derniers résultats publiés autour de la logique du premier ordre est “la décomposabilité” : une propriété partagée par plusieurs théories du premier ordre qui permet de dégager une procédure de décision générale qui pour toute proposition (formule sans variables libres) produit soit vrai soit faux dans toute théorie décomposable. Malheureusement, cette procédure de décision ne permet pas de résoudre des contraintes du premier ordre contenant des variables libres. Ce genre de problème est connu sous le nom de first-order constraint satisfaction problems. Nous présentons donc dans ce papier, le premier solveur complet de contraintes du premier ordre dans toute théorie décomposable T. L'idée principale est de combiner une propagation de sous-formules logiques avec des propriétés subtiles de la décomposabilité. Notre solveur est composé de neuf règles de réécriture qui transforme toute contrainte du premier ordre φ (qui peut évidement contenir des variables libres) en une formule équivalente Φ qui est : soit la formule vrai, soit la formule faux, soit une formule simple ayant au moins une variable libre et n'étant équivalente ni à vrai ni à faux. Nous montrons l'efficacité de notre solveur en résolvant des contraintes du premier ordre sur des arbres finis ou infinis contenant un grand nombre de quantificateurs imbriqués et comparons les performances obtenues avec ceux de notre tout dernier solveur de contraintes du premier ordre dédié aux arbres finis ou infinis. Ceci est le premier solveur de contraintes du premier ordre pour toute théorie décomposable T.
Type de document :
Communication dans un congrès
Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.349-360, 2008
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00294886
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : jeudi 10 juillet 2008 - 16:14:36
Dernière modification le : mercredi 29 novembre 2017 - 10:20:09
Document(s) archivé(s) le : vendredi 28 mai 2010 - 23:24:28

Fichier

pages-349-359-article5.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00294886, version 1

Collections

Citation

Khalil Djelloul. Combinaison de la propagation et de la décomposabilité pour la résolution de contraintes du premier ordre. Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.349-360, 2008. 〈inria-00294886〉

Partager

Métriques

Consultations de la notice

127

Téléchargements de fichiers

149