Name
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 |
|---|---|---|
1992 | 10.1007/3-540-55602-8_157 | CADE |
Keywords | Field | DocType |
extended abstract,combinatory logic approach,higher-order e-unification,logical framework,first order,higher order | Discrete mathematics,Lambda calculus,Complete Method,Combinatory logic,Computer science,Unification,Algorithm,Rewriting,Logical framework,Equational theory | Conference |
ISBN | Citations | PageRank |
3-540-55602-8 | 3 | 0.38 |
References | Authors | |
18 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniel J. Dougherty | 1 | 413 | 32.13 |
| Patricia Johann | 2 | 6 | 2.53 |