Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/inria-00085773
Contributor : Laurent Henocque <>
Submitted on : Friday, July 14, 2006 - 9:08:36 AM
Last modification on : Thursday, February 7, 2019 - 4:48:29 PM
Long-term archiving on: : Tuesday, April 6, 2010 - 12:07:59 AM

File

Identifiers

  • 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. ⟨inria-00085773⟩

Share

Metrics

Record views

234

Files downloads

68