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 |