Complétude des extensions en arbres de théories

Résumé : Nous présentons dans ce papier une méthode pour combiner une théorie T quelconque du premier ordre avec la théorie des arbres éventuellement infinis. Sémantiquement cette nouvelle théorie hybride n'est rien d'autre qu'une axiomatisation de l'extension en arbres des éléments des modèles de la théorie T. Tout d'abord, ayant une axiomatisation d'une théorie T, nous donnons l'axiomatisation de la théorie T de l'extension en arbre de T et présentons son modèle standard M. Nous introduisons ensuite une nouvelle classe de théories dite flexibles et montrons que si T est flexible alors T est complète. Les théories flexibles sont des théories ayant des propriétés élégantes qui nous permettent de manipuler aisément les formules. Enfin nous présentons un algorithme de décision de propositions dans T pour toute théorie T flexible. L'algorithme est donné sous forme d'un ensemble de six règles de réécriture qui pour toute proposition ' donnent soit vrai soit faux.
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 [7 références]  Voir  Masquer  Télécharger

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

Fichier

Identifiants

  • HAL Id : inria-00085774, version 1

Collections

Citation

Khalil Djelloul, Thi-Bich-Hanh Dao. Complétude des extensions en arbres de théories. Journées Francophones de Programmation par Contraintes, 2006, Nîmes - Ecole des Mines d'Alès, 2006. 〈inria-00085774〉

Partager

Métriques

Consultations de la notice

153

Téléchargements de fichiers

65