A Combinatory Logic Approach To Higher-order E-unification

ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
Patricia Johann Ph.D, Professor (Creator)
Appalachian State University (ASU )
Web Site: https://library.appstate.edu/

Abstract: Let E be a first-order equational theory. A translation of typed higher-order E-unification problems into a typed 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.

Additional Information

Dougherty, D. and Johann, P. (1995). A Combinatory Logic Approach To Higher-order E-unification. Theoretical Computer Science B 139, pp. 207-242. Publisher version of record available at: https://cs.appstate.edu/~johannp/tcs95.pdf
Language: English
Date: 1995
computer science, logic, combinatory logic, E-unification, equational theory

Email this document to