{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T04:49:24Z","timestamp":1649134164201},"reference-count":42,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1995,3,1]],"date-time":"1995-03-01T00:00:00Z","timestamp":794016000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":6713,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1995,3]]},"DOI":"10.1016\/0304-3975(94)00210-a","type":"journal-article","created":{"date-parts":[[2003,5,13]],"date-time":"2003-05-13T04:04:58Z","timestamp":1052798698000},"page":"207-242","source":"Crossref","is-referenced-by-count":4,"title":["A combinatory logic approach to higher-order E-unification"],"prefix":"10.1016","volume":"139","author":[{"given":"Daniel J.","family":"Dougherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patricia","family":"Johann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(94)00210-A_BIB1","series-title":"Proc. 2nd Internat. Workshop on Conditional and Typed Rewriting Systems, Center for Pattern Recognition and Machine Intelligence","article-title":"Adding algebraic rewriting to the calculus of constructions: strong normalization preserved, Extended Abstracts","author":"Barbanera","year":"1990"},{"key":"10.1016\/0304-3975(94)00210-A_BIB2","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1016\/0022-0000(86)90033-4","article-title":"Conditional rewrite rules: confluence and termination","volume":"32","author":"Bergstra","year":"1986","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/0304-3975(94)00210-A_BIB3","series-title":"Proc. 10th Conf. on Automated Deduction","first-page":"292","article-title":"Unification in a combination of equational theories: an efficient algorithm","volume":"Vol. 449","author":"Boudet","year":"1990"},{"key":"10.1016\/0304-3975(94)00210-A_BIB4","series-title":"Proc. 3rd Ann. IEEE Symp. on Logic in Computer Science","first-page":"82","article-title":"Combining algebra and higher-order types","author":"Breazu-Tannen","year":"1988"},{"key":"10.1016\/0304-3975(94)00210-A_BIB5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(91)90037-3","article-title":"Polymorphic rewriting conserves algebraic strong normalization","volume":"83","author":"Breazu-Tannen","year":"1989","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(94)00210-A_BIB6","volume":"Vol. I","author":"Curry","year":"1958"},{"key":"10.1016\/0304-3975(94)00210-A_BIB7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","article-title":"Termination of rewriting","volume":"3","author":"Dershowitz","year":"1987","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/0304-3975(94)00210-A_BIB8","first-page":"243","article-title":"Rewrite sytems","author":"Dershowitz","year":"1990"},{"key":"10.1016\/0304-3975(94)00210-A_BIB9","article-title":"Surjective pairing and strong normalization: two themes in lambda calculus","author":"deVrijer","year":"1987"},{"key":"10.1016\/0304-3975(94)00210-A_BIB10","article-title":"Unique normal forms for combinatory logic with parallel conditional, a case study in conditional rewriting","author":"deVrijer","year":"1990"},{"key":"10.1016\/0304-3975(94)00210-A_BIB11_1","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/0890-5401(92)90064-M","article-title":"Adding algebra to the untyped lambda calculus","volume":"101","author":"Dougherty","year":"1992","journal-title":"Inform. and Comput."},{"key":"10.1016\/0304-3975(94)00210-A_BIB11_2","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/0890-5401(92)90064-M","article-title":"Adding algebra to the untyped lambda calculus","volume":"102","author":"Dougherty","year":"1992","journal-title":"Inform. and Comput."},{"key":"10.1016\/0304-3975(94)00210-A_BIB12","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0304-3975(93)90075-5","article-title":"Higher-order unification via combinators","volume":"114","author":"Dougherty","year":"1993","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(94)00210-A_BIB13","series-title":"Proc. 3rd Internat. Conf. on Rewriting Techniques and Applications","first-page":"121","article-title":"Higher-order unification with dependent function types","volume":"Vol. 355","author":"Elliott","year":"1989"},{"key":"10.1016\/0304-3975(94)00210-A_BIB14","series-title":"Technical Report CMU-CS-90-134","article-title":"Extensions and applications of higher-order unification","author":"Elliott","year":"1990"},{"key":"10.1016\/0304-3975(94)00210-A_BIB15","series-title":"eLP: A common Lisp implementation of \u03bb-Prolog in the Ergo support system","author":"Elliott","year":"1989"},{"key":"10.1016\/0304-3975(94)00210-A_BIB16","series-title":"Proc. 4th Workshop on Automated Deduction","first-page":"161","article-title":"First order unification in an equational theory","volume":"Vol. 87","author":"Fay","year":"1979"},{"key":"10.1016\/0304-3975(94)00210-A_BIB17","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","article-title":"Complete sets of transformations for general E-unification","volume":"67","author":"Gallier","year":"1989","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(94)00210-A_BIB18","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","article-title":"Higher-order unification revisited: complete sets of transformations","volume":"8","author":"Gallier","year":"1989","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/0304-3975(94)00210-A_BIB19","doi-asserted-by":"crossref","first-page":"224","DOI":"10.2307\/2271660","article-title":"Axioms for strong reduction in combinatory logic","volume":"32","author":"Hindley","year":"1967","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/0304-3975(94)00210-A_BIB20","first-page":"808","article-title":"A short proof of Curry's normal form theorem","volume":"24","author":"Hindley","year":"1970"},{"key":"10.1016\/0304-3975(94)00210-A_BIB21","series-title":"Introduction to Combinators and \u03bb-Calculus","author":"Hindley","year":"1986"},{"key":"10.1016\/0304-3975(94)00210-A_BIB22","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","article-title":"A unification algorithm for typed \u03bb-calculus","volume":"1","author":"Huet","year":"1975","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(94)00210-A_BIB23","article-title":"A complete transformation system for polymorphic higher-order unification","author":"Hustadt","year":"1991"},{"key":"10.1016\/0304-3975(94)00210-A_BIB24","article-title":"Complete sets of transaformations for unification problems","author":"Johann","year":"1991"},{"key":"10.1016\/0304-3975(94)00210-A_BIB25","doi-asserted-by":"crossref","DOI":"10.1305\/ndjfl\/1040408614","article-title":"Normal forms in combinatory logic","author":"Johann","year":"1992"},{"key":"10.1016\/0304-3975(94)00210-A_BIB26","series-title":"Computational Logic: Essays in Honour of Alan Robinson","first-page":"257","article-title":"Solving equations in abstract algebras: a rule-based study of unification","author":"Jouannaud","year":"1991"},{"key":"10.1016\/0304-3975(94)00210-A_BIB27","series-title":"Proc. 6th Ann. IEEE Symp. on Logic in Computer Science","first-page":"350","article-title":"A computation model for executable higher-order algebraic specification languages","author":"Jounnaud","year":"1991"},{"key":"10.1016\/0304-3975(94)00210-A_BIB28","article-title":"Combinatory reduction systems","author":"Klop","year":"1980","journal-title":"Mathematical Center Tracts 129"},{"key":"10.1016\/0304-3975(94)00210-A_BIB29","doi-asserted-by":"crossref","first-page":"237","DOI":"10.2307\/2271661","article-title":"The decidability of Hindley's axioms for strong reduction","volume":"32","author":"Lercher","year":"1967","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0304-3975(94)00210-A_BIB30","doi-asserted-by":"crossref","first-page":"213","DOI":"10.2307\/2271659","article-title":"Strong reduction and normal form in combinatory logic","volume":"32","author":"Lercher","year":"1967","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0304-3975(94)00210-A_BIB31","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","article-title":"An efficient unification algorithm","volume":"4","author":"Martelli","year":"1982","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"10.1016\/0304-3975(94)00210-A_BIB32","first-page":"365","article-title":"Type systems for programming languages","author":"Mitchell","year":"1990"},{"key":"10.1016\/0304-3975(94)00210-A_BIB33","series-title":"Proc. 2nd Internat. Workshop on Conditional and Typed Rewriting Systems, Center for Pattern Recognition and Machine Intelligence","article-title":"Higher-order unification, polymorphism and subsorts, Extended Abstracts","author":"Nipkow","year":"1990"},{"key":"10.1016\/0304-3975(94)00210-A_BIB34","series-title":"Proc. 4th Internat. Conf. on Rewriting Techniques and Applications","first-page":"200","article-title":"Modular higher-order E-unification","volume":"Vol. 488","author":"Nipkow","year":"1991"},{"key":"10.1016\/0304-3975(94)00210-A_BIB35","series-title":"Proc. ISSAC89","article-title":"Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent rewrite system","author":"Okada","year":"1989"},{"key":"10.1016\/0304-3975(94)00210-A_BIB36","series-title":"The Implementation of Functional Programming Languages","author":"Peyton-Jones","year":"1987"},{"key":"10.1016\/0304-3975(94)00210-A_BIB37","series-title":"Proc. of SIGPLAN88 Symp. on Language Design and Implementation","first-page":"199","article-title":"Higher-order abstract syntax","author":"Pfenning","year":"1988"},{"key":"10.1016\/0304-3975(94)00210-A_BIB38","series-title":"Proc. 2nd Internat. Conf. on Rewriting Techniques and Applications","article-title":"Improving basic narrowing techniques","author":"R\u00e9ty","year":"1987"},{"key":"10.1016\/0304-3975(94)00210-A_BIB39","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","article-title":"Unification in a combination of arbitrary disjoint equational theories","volume":"8","author":"Schmidt-Schauss","year":"1989","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/0304-3975(94)00210-A_BIB40","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","article-title":"Unification theory","volume":"7","author":"Siekmann","year":"1989","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/0304-3975(94)00210-A_BIB41","series-title":"Proc. 10th Conf. on Automated Deduction","first-page":"292","article-title":"Higher-order E-unification","volume":"Vol. 449","author":"Snyder","year":"1990"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759400210A?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759400210A?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T12:27:27Z","timestamp":1555417647000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030439759400210A"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,3]]},"references-count":42,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1995,3]]}},"alternative-id":["030439759400210A"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(94)00210-a","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1995,3]]}}}