Extension au premier ordre de l'unification des termes par CHR

Résumé : Prolog, acronyme de PROgrammation LOGique, est lÕun des principaux langages de programmation logique. Un de ces concepts de base est \emph{l'unification des ter mes} qui consiste à instancier les variables de deux termes afin que ces derniers soient syntaxiquement égaux. Techniquement parlant, l'unification est équivalente à la résolution de conjonctions d'équations dans la théorie des arbres finis ou infinis. Nous présentons dans ce papier une extension au premier ordre du mécanisme de l'unification des termes par un algorithme de résolution de contraintes du premier ordre (toute quantification et t out symbole logique) dans une théorie étendue $T$ d'arbres finis ou infini s. Pour cela, nous étendons tout d'abord la théorie des arbres finis ou in finis par la relation $\fini(t)$ qui permet de contraindre le terme $t$ à être un arbre fini et présentons une axiomatisation au premier ordre de cette théorie étendue. Nous montrons ensuite la complétude de $T$ par un solveur de contraintes du premier ordre sous forme de 16 règles de réécriture. Nous terminons ce papier par une implémentation en CHR de notre solveur. CHR (Constraint Handling Rules) est un langage de programmation logique à base de règles de réécriture qui a fait ses preuves dans la résolution de plusieurs problèmes complexes en IA. Cependant, il n'existe à c e jour aucun solveur CHR de contraintes du premier ordre. La complexité et l a puissance de nos 16 règles de réécriture posent un véritable challenge pour CHR et ses programmeurs. Nous montrons alors comment représenter en CHR la structure complexe des formules du premier ordre et comment traduire chaque règle de notre solveur en règles CHR afin d'obtenir le premier solveur CHR de contraintes du premier ordre !
Type de document :
Communication dans un congrès
Troisièmes Journées Francophones de Programmationpar Contraintes (JFPC07), Jun 2007, INRIA, Domaine de Voluceau, Rocquencourt, Yvelines France, 2007, JFPC07
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00151075
Contributeur : Sylvain Soliman <>
Soumis le : vendredi 1 juin 2007 - 15:32:49
Dernière modification le : mercredi 29 novembre 2017 - 10:19:27
Document(s) archivé(s) le : vendredi 21 septembre 2012 - 16:06:50

Fichier

52.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00151075, version 1

Collections

Citation

Khalil Djelloul, Thi-Bich-Hanh Dao, Thom Fruehwirth. Extension au premier ordre de l'unification des termes par CHR. Troisièmes Journées Francophones de Programmationpar Contraintes (JFPC07), Jun 2007, INRIA, Domaine de Voluceau, Rocquencourt, Yvelines France, 2007, JFPC07. 〈inria-00151075〉

Partager

Métriques

Consultations de la notice

146

Téléchargements de fichiers

85