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

{"_id":{"_str":"51f6934359ced8df44000e46"},"__v":1,"authorIDs":[],"author_short":["Dougherty, D.<nbsp>J.\\","Johann, P."],"bibbaseid":"dougherty-johann-acombinatorylogicapproachtohigherordereunification-1995","bibdata":{"html":"<div class=\"bibbase_paper\"> \n\n\n<span class=\"bibbase_paper_titleauthoryear\">\n\t<span class=\"bibbase_paper_title\"><a name=\"a_tcs95\"> </a>A combinatory logic approach to higher-order $E$-unification.</span>\n\t<span class=\"bibbase_paper_author\">\nDougherty, D.&nbsp;J.\\; and Johann, P.</span>\n\t<!-- <span class=\"bibbase_paper_year\">1995</span>. -->\n</span>\n\n\n\n<i>Theoretical Computer Science</i>,\n\n139(1--2):207--242.\n\n 1995.\n\n\n\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content\">\n \n \n <!-- <i -->\n <!-- onclick=\"javascript:log_download('dougherty-johann-acombinatorylogicapproachtohigherordereunification-1995', 'http://web.cs.wpi.edu/~dd/publications/tcs95.pdf')\">DEBUG -->\n <!-- </i> -->\n\n <a href=\"http://web.cs.wpi.edu/~dd/publications/tcs95.pdf\"\n onclick=\"javascript:log_download('dougherty-johann-acombinatorylogicapproachtohigherordereunification-1995', 'http://web.cs.wpi.edu/~dd/publications/tcs95.pdf')\">\n <img src=\"http://bibbase.org/img/filetypes/pdf.png\"\n\t alt=\"A combinatory logic approach to higher-order $E$-unification [.pdf]\" \n\t class=\"bibbase_icon\"\n\t style=\"width: 24px; height: 24px; border: 0px; vertical-align: text-top\" ><span class=\"bibbase_icon_text\">Paper</span></a> \n &nbsp;\n \n \n <a href=\"javascript:showBib('a_tcs95')\"\n class=\"bibbase link\">\n <!-- <img src=\"http://bibbase.org/img/filetypes/bib.png\" -->\n\t<!-- alt=\"A combinatory logic approach to higher-order $E$-unification [bib]\" -->\n\t<!-- class=\"bibbase_icon\" -->\n\t<!-- style=\"width: 24px; height: 24px; border: 0px; vertical-align: text-top\"><span class=\"bibbase_icon_text\">Bibtex</span> -->\n BibTeX\n <i class=\"fa fa-caret-down\"></i></a>\n \n \n &nbsp;\n <a class=\"bibbase_abstract_link bibbase link\"\n href=\"javascript:showAbstract('a_tcs95')\">\n Abstract\n <i class=\"fa fa-caret-down\"></i></a>\n \n \n \n\n \n \n \n</span>\n\n<div class=\"well well-small bibbase\" id=\"bib_a_tcs95\"\n style=\"display:none\">\n <pre>@article{ a_tcs95,\n author = {Daniel J.\\ Dougherty and Patricia Johann},\n title = {A combinatory logic approach to higher-order\n {$E$}-unification},\n journal = {Theoretical Computer Science},\n volume = {139},\n number = {1--2},\n pages = {207--242},\n day = {06},\n year = {1995},\n issn = {0304-3975},\n pubcountry = {Netherlands},\n abstract = {Let E be a first-order equational theory. A\n translation of typed higher-order E-unification\n problems into a typed combinatory logic\n framework is presented and justified. The case\n in which E admits presentation as a convergent\n term rewriting system is treated in detail: in\n this situation, a modification of ordinary\n narrowing is shown to be a complete method for\n enumerating higher-order E-unifiers. In fact,\n we treat a more general problem, in which the\n types of terms contain type variables. },\n url = {tcs95.pdf}\n}</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" id=\"abstract_a_tcs95\"\n style=\"display:none\">\n 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.\n</div>\n\n\n</div>\n","downloads":0,"bibbaseid":"dougherty-johann-acombinatorylogicapproachtohigherordereunification-1995","urls":{"Paper":"http://web.cs.wpi.edu/~dd/publications/tcs95.pdf"},"role":"author","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.","author":["Dougherty, Daniel J.\\","Johann, Patricia"],"author_short":["Dougherty, D.<nbsp>J.\\","Johann, P."],"bibtex":"@article{ a_tcs95,\n author = {Daniel J.\\ Dougherty and Patricia Johann},\n title = {A combinatory logic approach to higher-order\n {$E$}-unification},\n journal = {Theoretical Computer Science},\n volume = {139},\n number = {1--2},\n pages = {207--242},\n day = {06},\n year = {1995},\n issn = {0304-3975},\n pubcountry = {Netherlands},\n abstract = {Let E be a first-order equational theory. A\n translation of typed higher-order E-unification\n problems into a typed combinatory logic\n framework is presented and justified. The case\n in which E admits presentation as a convergent\n term rewriting system is treated in detail: in\n this situation, a modification of ordinary\n narrowing is shown to be a complete method for\n enumerating higher-order E-unifiers. In fact,\n we treat a more general problem, in which the\n types of terms contain type variables. },\n url = {tcs95.pdf}\n}","bibtype":"article","day":"06","id":"a_tcs95","issn":"0304-3975","journal":"Theoretical Computer Science","key":"a_tcs95","number":"1--2","pages":"207--242","pubcountry":"Netherlands","title":"A combinatory logic approach to higher-order $E$-unification","type":"article","url":"tcs95.pdf","volume":"139","year":"1995"},"bibtype":"article","biburl":"http://web.cs.wpi.edu/~dd/publications/index.bib","downloads":0,"search_terms":["combinatory","logic","approach","higher","order","unification","dougherty","johann"],"title":"A combinatory logic approach to higher-order $E$-unification","year":1995,"dataSources":["HB5RrPb3Y5aikRoLH"]}