Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/inria-00294886
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Submitted on : Thursday, July 10, 2008 - 4:14:36 PM
Last modification on : Thursday, February 7, 2019 - 3:04:36 PM
Long-term archiving on: : Friday, May 28, 2010 - 11:24:28 PM

File

pages-349-359-article5.pdf
Files produced by the author(s)

Identifiers

  • 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. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, LINA - Université de Nantes - Ecole des Mines de Nantes, Jun 2008, Nantes, France. pp.349-360. ⟨inria-00294886⟩

Share

Metrics

Record views

160

Files downloads

216