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)
- Institution
- 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.
A Combinatory Logic Approach To Higher-order E-unification
PDF (Portable Document Format)
503 KB
Created on 10/19/2021
Views: 749
Additional Information
- Publication
- 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
- Keywords
- computer science, logic, combinatory logic, E-unification, equational theory