Paper  abstract   bibtex   

@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}
}