A COMBINATORY-LOGIC APPROACH TO HIGHER-ORDER E-UNIFICATION

被引：2
|
作者：
DOUGHERTY, DJ
JOHANN, P
机构：
[1] HOBART & WILLIAM SMITH COLL, DEPT MATH & COMP SCI, GENEVA, NY 14456 USA
[2] WESLEYAN UNIV, DEPT MATH, MIDDLETOWN, CT 06457 USA
来源：
THEORETICAL COMPUTER SCIENCE | 1995年 / 139卷 / 1-2期
关键词：
D O I：
10.1016/0304-3975(94)00210-A
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：207 / 242
页数：36
相关论文
共 50 条
12345