E-unification by means of tree tuple synchronized grammars
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Discrete Mathematics & Theoretical Computer Science
1997-12-01
|
| Series: | Discrete Mathematics & Theoretical Computer Science |
| Online Access: | http://www.dmtcs.org/dmtcs-ojs/index.php/dmtcs/article/view/77 |
| _version_ | 1818192023815979008 |
|---|---|
| author | Sébastien Limet Pierre Réty |
| author_facet | Sébastien Limet Pierre Réty |
| author_sort | Sébastien Limet |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-12T00:23:55Z |
| format | Article |
| id | doaj.art-76bf178ab0a94c4ca89986b2748c9bea |
| institution | Directory Open Access Journal |
| issn | 1462-7264 1365-8050 |
| language | English |
| last_indexed | 2024-12-12T00:23:55Z |
| publishDate | 1997-12-01 |
| publisher | Discrete Mathematics & Theoretical Computer Science |
| record_format | Article |
| series | Discrete Mathematics & Theoretical Computer Science |
| spelling | doaj.art-76bf178ab0a94c4ca89986b2748c9bea2022-12-22T00:44:39ZengDiscrete Mathematics & Theoretical Computer ScienceDiscrete Mathematics & Theoretical Computer Science1462-72641365-80501997-12-0111E-unification by means of tree tuple synchronized grammarsSébastien LimetPierre RétyThe 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.http://www.dmtcs.org/dmtcs-ojs/index.php/dmtcs/article/view/77 |
| spellingShingle | Sébastien Limet Pierre Réty E-unification by means of tree tuple synchronized grammars Discrete Mathematics & Theoretical Computer Science |
| title | E-unification by means of tree tuple synchronized grammars |
| title_full | E-unification by means of tree tuple synchronized grammars |
| title_fullStr | E-unification by means of tree tuple synchronized grammars |
| title_full_unstemmed | E-unification by means of tree tuple synchronized grammars |
| title_short | E-unification by means of tree tuple synchronized grammars |
| title_sort | e unification by means of tree tuple synchronized grammars |
| url | http://www.dmtcs.org/dmtcs-ojs/index.php/dmtcs/article/view/77 |
| work_keys_str_mv | AT sebastienlimet eunificationbymeansoftreetuplesynchronizedgrammars AT pierrerety eunificationbymeansoftreetuplesynchronizedgrammars |