E-unification by means of tree tuple synchronized grammars
Discrete mathematics & theoretical computer science, Tome 1 (1997).

Voir la notice de l'article provenant de la source Episciences

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.
@article{DMTCS_1997_1_a9,
     author = {Limet, S\'ebastien and R\'ety, Pierre},
     title = {E-unification by means of tree tuple synchronized grammars},
     journal = {Discrete mathematics & theoretical computer science},
     publisher = {mathdoc},
     volume = {1},
     year = {1997},
     doi = {10.46298/dmtcs.240},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.46298/dmtcs.240/}
}
TY  - JOUR
AU  - Limet, Sébastien
AU  - Réty, Pierre
TI  - E-unification by means of tree tuple synchronized grammars
JO  - Discrete mathematics & theoretical computer science
PY  - 1997
VL  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/articles/10.46298/dmtcs.240/
DO  - 10.46298/dmtcs.240
LA  - en
ID  - DMTCS_1997_1_a9
ER  - 
%0 Journal Article
%A Limet, Sébastien
%A Réty, Pierre
%T E-unification by means of tree tuple synchronized grammars
%J Discrete mathematics & theoretical computer science
%D 1997
%V 1
%I mathdoc
%U http://geodesic.mathdoc.fr/articles/10.46298/dmtcs.240/
%R 10.46298/dmtcs.240
%G en
%F DMTCS_1997_1_a9
Limet, Sébastien; Réty, Pierre. E-unification by means of tree tuple synchronized grammars. Discrete mathematics & theoretical computer science, Tome 1 (1997). doi : 10.46298/dmtcs.240. http://geodesic.mathdoc.fr/articles/10.46298/dmtcs.240/

Cité par Sources :