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

Citation
Dj. Dougherty et P. Johann, A COMBINATORY-LOGIC APPROACH TO HIGHER-ORDER E-UNIFICATION, Theoretical computer science, 139(1-2), 1995, pp. 207-242
Citations number
42
Categorie Soggetti
Computer Sciences","Computer Science Theory & Methods
ISSN journal
03043975
Volume
139
Issue
1-2
Year of publication
1995
Pages
207 - 242
Database
ISI
SICI code
0304-3975(1995)139:1-2<207:ACATHE>2.0.ZU;2-U
Abstract
Let E be a first-order equational theory. A translation of higher-orde r E-unification problems into a combinatory logic framework is present ed and justified. The case in which E admits presentation as a converg ent term rewriting system is treated in detail: in this situation, a m odification 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.