Discrete Mathematics & Theoretical Computer Science
Volume 1 n° 1 (1997), pp. 69-98
| author: | Sébastien Limet and Pierre Réty |
|---|---|
| title: | E-unification by means of tree tuple synchronized grammars |
| keywords: | E-unification, narrowing, tree languages, decidability |
| 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. |
| reference: | Sébastien Limet and Pierre Réty (1997), E-unification by means of tree tuple synchronized grammars, Discrete Mathematics and Theoretical Computer Science 1, pp. 69-98 |
| ps.gz-source: | dm010105.ps.gz |
| ps-source: | dm010105.ps ( 307 K ) |
| pdf-source: | dm010105.pdf ( 391 K ) |
The first source gives you the `gzipped' PostScript, the second the plain PostScript and the third the format for the Adobe accrobat reader. Depending on the installation of your web browser, at least one of these should (after some amount of time) pop up a window for you that shows the full article. If this is not the case, you should contact your system administrator to install your browser correctly.
Automatically produced on Tue Jan 19 17:48:59 MET 1999 by gustedt