A combinatory logic approach to higher-order $E$-unification. Dougherty, D. J.\ and Johann, P. Theoretical Computer Science, 139(1--2):207--242, 1995.
A combinatory logic approach to higher-order $E$-unification [pdf]Paper  abstract   bibtex   
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.
@article{ a_tcs95,
  author = {Daniel J.\ Dougherty and Patricia Johann},
  title = {A combinatory logic approach to higher-order
                  {$E$}-unification},
  journal = {Theoretical Computer Science},
  volume = {139},
  number = {1--2},
  pages = {207--242},
  day = {06},
  year = {1995},
  issn = {0304-3975},
  pubcountry = {Netherlands},
  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. },
  url = {tcs95.pdf}
}
Downloads: 0