Abstract
For finite convergent term-rewriting systems it is shown that the equational unification problem is recursively independent of the equational matching problem, the word matching problem, and the 2nd-order equational matching problem. Apart from the latter these results are derived by considering term-rewriting systems on signatures that contain unary function symbols only (i.e., string-rewriting systems). Also for this special case 2nd-order equational matching is shown to be reducible to 1st-order equational matching. In addition, we present some new decidability results for simultaneous equational matching and unification. Finally, we compare the word unification problem to the 2nd-order equational unification problem.
| Original language | English |
|---|---|
| Pages (from-to) | 1-47 |
| Number of pages | 47 |
| Journal | Theoretical Computer Science |
| Volume | 198 |
| Issue number | 1-2 |
| DOIs | |
| State | Published - May 30 1998 |
Keywords
- 2nd-order equational matching and unification
- Equational matching and unification
- String-rewriting systems
- Term-rewriting systems
Fingerprint
Dive into the research topics of 'Equational unification, word unification, and 2nd-order equational unification'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver