Abstract | ||
---|---|---|
Let E be a first-order equational theory. A translation of higher-order E -unification problems into a combinatory logic framework is presented and justified. The case in which E admits presentation as a convergent term rewriting system is treated in detail: in this situation, a modification of ordinary narrowing is shown to be a complete method for enumerating higher-order E -unifiers. In fact, we treat a more general problem, in which the types of terms contain type variables. |
Year | DOI | Venue |
---|---|---|
1995 | 10.1016/0304-3975(94)00210-A | Theor. Comput. Sci. |
Keywords | DocType | Volume |
combinatory logic approach | Journal | 139 |
Issue | ISSN | Citations |
1-2 | Theoretical Computer Science | 1 |
PageRank | References | Authors |
0.43 | 7 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Daniel J. Dougherty | 1 | 413 | 32.13 |
Patricia Johann | 2 | 1 | 0.43 |