Résolution de contraintes du premier ordre dans la théorie des arbres évalués

Résumé : Nous présentons dans ce papier un algorithme général de résolution de contraintes du premier ordre dans la théorie T des arbres évalués. Cette théorie est une combinaison de la théorie des arbres finis ou infinis et de la théorie des rationnels munis de l'addition, de la soustraction et d'une relation d'ordre dense sans extrême. L'algorithme est donné sous forme d'un ensemble de 28 règles de réécriture et transforme toute formule du premier ordre ', qui peut éventuellement contenir des variables libres, en une disjonction D de formules résolues, équivalente à ' dans T, sans nouvelles variables libres, et telle que D est soit la formule vrai , soit la formule faux , soit une formule ayant au moins une variable libre et n'étant équivalente ni à vrai ni à faux dans T. En particulier, si ' est sans variables libres, D est soit la formule vrai soit la formule faux . Si D contient des variables libres, les solutions sur ces variables sont exprimées d'une façon explicite et D peut se transformer directement en une combinaison booléenne de conjonctions quantifiées de formules atomiques, qui n'acceptent pas d'élimination de quantificateurs. La correction de notre algorithme est une autre preuve de la complétude de la théorie T.
Type de document :
Communication dans un congrès
Journées Francophones de Programmation par Contraintes, 2006, Nîmes - Ecole des Mines d'Alès, 2006
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00085773
Contributeur : Laurent Henocque <>
Soumis le : vendredi 14 juillet 2006 - 09:08:36
Dernière modification le : vendredi 9 mars 2018 - 11:25:58
Document(s) archivé(s) le : mardi 6 avril 2010 - 00:07:59

Fichier

Identifiants

  • HAL Id : inria-00085773, version 1

Collections

Citation

Thi-Bich-Hanh Dao, Khalil Djelloul. Résolution de contraintes du premier ordre dans la théorie des arbres évalués. Journées Francophones de Programmation par Contraintes, 2006, Nîmes - Ecole des Mines d'Alès, 2006. 〈inria-00085773〉

Partager

Métriques

Consultations de la notice

196

Téléchargements de fichiers

35