E-unification by means of tree tuple synchronized grammars

Abstract : The goal of this paper is both to give an E-unification procedure that always terminates, and to decide unifiability. For this, we assume that the equational theory is specified by a confluent and constructor-based rewrite system, and that four additional restrictions are satisfied. We give a procedure that represents the (possibly infinite) set of solutions thanks to a tree tuple synchronized grammar, and that can decide upon unifiability thanks to an emptiness test. Moreover, we show that if only three of the four additional restrictions are satisfied then unifiability is undecidable.
Type de document :
Article dans une revue
Discrete Mathematics and Theoretical Computer Science, DMTCS, 1997, 1, pp.69-98
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00955691
Contributeur : Alain Monteil <>
Soumis le : mercredi 5 mars 2014 - 09:31:17
Dernière modification le : mercredi 29 novembre 2017 - 10:26:23
Document(s) archivé(s) le : jeudi 5 juin 2014 - 10:52:26

Fichier

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

Identifiants

  • HAL Id : hal-00955691, version 1

Collections

Citation

Sébastien Limet, Pierre Réty. E-unification by means of tree tuple synchronized grammars. Discrete Mathematics and Theoretical Computer Science, DMTCS, 1997, 1, pp.69-98. 〈hal-00955691〉

Partager

Métriques

Consultations de la notice

172

Téléchargements de fichiers

247