{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:19:37Z","timestamp":1725664777570},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614647"},{"type":"electronic","value":"9783540685968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61464-8_63","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:40:12Z","timestamp":1330292412000},"page":"332-346","source":"Crossref","is-referenced-by-count":35,"title":["Linear second-order unification"],"prefix":"10.1007","author":[{"given":"Jordi","family":"Levy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"26_CR1","unstructured":"H. Comon. Completion of rewrite systems with membership constraints, part I: Deduction rules and part II: Constraint solving. Technical report, CNRS and LRI, Universit\u00e9 de Paris Sud, 1993. (To appear in J. of Symbolic Computation)."},{"key":"26_CR2","first-page":"273","volume":"40","author":"J. H. Gallier","year":"1990","unstructured":"J. H. Gallier and W. Snyder. Designing unification procedures using transformations: A survey. Bulletin of the EATCS, 40:273\u2013326, 1990.","journal-title":"Bulletin of the EATCS"},{"key":"26_CR3","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W. D. Goldfarb","year":"1981","unstructured":"W. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225\u2013230, 1981.","journal-title":"Theoretical Computer Science"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"W. E. Gould. A Matching Procedure for \u03c9-Order Logic. PhD thesis, Princeton Univ., 1966.","DOI":"10.21236\/AD0646560"},{"issue":"3","key":"26_CR5","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"G. Huet","year":"1973","unstructured":"G. Huet. The undecidability of unification in third-order logic. Information and Control, 22(3):257\u2013267, 1973.","journal-title":"Information and Control"},{"key":"26_CR6","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"26_CR7","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0304-3975(76)90021-9","volume":"3","author":"D. C. Jensen","year":"1976","unstructured":"D. C. Jensen and T. Pietrzykowski. Mechanizing \u03c9-order type theory through unification. Theoretical Computer Science, 3:123\u2013171, 1976.","journal-title":"Theoretical Computer Science"},{"key":"26_CR8","first-page":"17","volume":"690","author":"J. Levy","year":"1993","unstructured":"J. Levy and J. Agust\u00ed. Bi-rewriting, a term rewriting technique for monotonic order relations. In 4th Int. Conf. on Rewriting Techniques and Applications, RTA'93, volume 690 of LNCS, pages 17\u201331, Montreal, Canada, 1993.","journal-title":"LNCS"},{"key":"26_CR9","unstructured":"J. Levy and J. Agust\u00ed. Bi-rewriting systems. J. of Symbolic Computation, 1995. (To be published)."},{"key":"26_CR10","unstructured":"C. Lor\u00eda-S\u00e1enz. A Theoretical Framework for Reasoning about Program Construction based on Extensions of Rewrite Systems. PhD thesis, Univ. Kaiserslautern, 1993."},{"key":"26_CR11","unstructured":"C. L. Lucchesi. The undecidability of the unification problem for third-order languages. Technical Report CSRR 2059, Dept. of Applied Analysis and Computer Science, Univ. of Waterloo, 1972."},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"O. Lysne and J. Piris. A termination ordering for higher-order rewrite systems. In 6th Int. Conf on Rewriting Techniques and Applications, RTA'95, volume 914 of LNCS, Kaiserslautern, Germany, 1995.","DOI":"10.1007\/3-540-59200-8_45"},{"key":"26_CR13","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation, 1:497\u2013536, 1991.","journal-title":"J. of Logic and Computation"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Functional unification of higher-order patterns. In 8th IEEE Symp. on Logic in Computer Science, LICS'93, pages 64\u201374, Montreal, Canada, 1993.","DOI":"10.1109\/LICS.1993.287599"},{"issue":"2","key":"26_CR15","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/321752.321764","volume":"20","author":"T. Pietrzykowski","year":"1973","unstructured":"T. Pietrzykowski. A complete mechanization of second-order logic. J. of the ACM, 20(2):333\u2013364, 1973.","journal-title":"J. of the ACM"},{"key":"26_CR16","unstructured":"C. Prehofer. Solving Higher-Order Equations: From Logic to Programming. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, 1995."},{"key":"26_CR17","volume-title":"Technical Report 12\/94","author":"M. Schmidt-Schau\u00df","year":"1995","unstructured":"M. Schmidt-Schau\u00df. Unification of stratified second-order terms. Technical Report 12\/94, Johan Wolfgang-Goethe-Universit\u00e4t, Frankfurt, Germany, 1995."},{"key":"26_CR18","unstructured":"K. U. Schulz. Makanin's algorithm, two improvements and a generalization. Technical Report CIS-Bericht-91-39, Centrum f\u00fcr Informations und Sprachverarbeitung, Universit\u00e4t M\u00fcnchen, 1991."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61464-8_63.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:06:32Z","timestamp":1605647192000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_63"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_63","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}