{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T05:14:12Z","timestamp":1737609252407,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_6","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T20:53:07Z","timestamp":1194641587000},"page":"82-96","source":"Crossref","is-referenced-by-count":8,"title":["Complexity of the Higher Order Matching"],"prefix":"10.1007","author":[{"given":"ToMasz","family":"Wierzbicki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1093\/oso\/9780198537618.003.0002","volume-title":"Handbook of Logic in Comput. Sci.","author":"H. Barendregt","year":"1992","unstructured":"Henk Barendregt, Lambda Calculi with Types, Handbook of Logic in Comput. Sci., vol. 2, S. Abramsky, D.M. Gabbay, T.S.E. Maibaum, eds., Clarendon Press, Oxford, 1992, 118\u2013310."},{"key":"6_CR2","unstructured":"Lewis D. Baxter, The Complexity of Unification, Ph.D. Thesis, University of Waterloo, 1976."},{"key":"6_CR3","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/BF01459101","volume":"99","author":"P. Bernays","year":"1928","unstructured":"Paul Bernays, Moses Sch\u00f6nfinkel, Zum Entscheidungsproblem der mathematischen Logik, Math. Annalen, 99 (1928) 342\u2013372.","journal-title":"Math. Annalen"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Egon B\u00f6rger, Erich Gr\u00e4del, Yuri Gurevich, The Classical Decision Problem, Springer-Verlag, 1997.","DOI":"10.1007\/978-3-642-59207-2"},{"key":"6_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027094","volume-title":"Proc. 11th Int\u2019l Workshop on Comput. Sci. Logic, CSL\u201997","author":"H. Comon","year":"1998","unstructured":"Hubert Comon, Yan Jurski, Higher order pattern matching and tree automata, Proc. 11th Int\u2019l Workshop on Comput. Sci. Logic, CSL\u201997, Aarhus, Denmark, August 23-29, 1997, M. Nielsen, W. Thomas, eds., LNCS 1414, Springer-Verlag, 1998."},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Gilles Dowek, Third order matching is decidable, Proc. 7th IEEE Symp. Logic in Comput. Sci., LICS\u201992, Santa Cruz, California, June 22-25, 1992, 2\u201310, also in Annals of Pure and Applied Logic, 69 (1994), 135-155.","DOI":"10.1016\/0168-0072(94)90083-3"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1016\/0304-3975(93)90175-S","volume":"107","author":"G. Dowek","year":"1993","unstructured":"Gilles Dowek, The undecidability of pattern matching in calculi where primitive recursive functionals are representable, Theoret. Comput. Sci., 107(1993) 349\u201356.","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"6_CR8","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0743-1066(84)90022-0","volume":"1","author":"C. Dwork","year":"1984","unstructured":"Cynthia Dwork, Paris C. Kanellakis, John C. Mitchell, On the sequential nature of unification, J. Logic Programming, 1(1) (1984) 35\u201350.","journal-title":"J. Logic Programming"},{"key":"6_CR9","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W. D. Goldfarb","year":"1981","unstructured":"Warren D. Goldfarb, Note on the undecidability of the second order unification problem, Theoret. Comput. Sci. 13(1981) 225\u2013230.","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"6_CR10","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. P. Huet","year":"1975","unstructured":"Gerard P. Huet, A unification algorithm for typed \u03bb-calculus, Theoret. Comput. Sci., 1 (1) (1975) 27\u201357.","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR11","unstructured":"Gerard P. Huet, R\u00e9solution d\u2019\u00e9quations dans des langages d\u2019ordre 1, 2,..., w. Th\u00e8se de Doctorat d\u2019\u00c9tat, University of Paris, 1976."},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. P. Huet","year":"1978","unstructured":"Gerard P. Huet, Bernard Lang, Proving and applying program transformations expressed with second order patterns, Acta Informatica, 11 (1978) 31\u201355.","journal-title":"Acta Informatica"},{"key":"6_CR13","unstructured":"Ralph Loader, The undecidability of \u03bb-definability, Church Memorial Volume, A. Anderson, M. Zeleny eds., Kluwer Acad. Press, to appear."},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1016\/0304-3975(92)90020-G","volume":"103","author":"H. G. Mairson","year":"1992","unstructured":"Harry G. Mairson, A simple proof of a theorem of Statman, Theoret. Comput. Sci., 103 (1992) 387\u2013394.","journal-title":"Theoret. Comput. Sci."},{"issue":"4","key":"6_CR15","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Dale Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, J. Logic and Comput., 1(4) (1991) 497\u2013536.","journal-title":"J. Logic and Comput."},{"key":"6_CR16","unstructured":"Vincent Padovani, Filtrage d\u2019ordre sup\u00e9rieur, PhD Thesis, Universit\u00e9 Paris VII, 1996."},{"key":"6_CR17","unstructured":"Christos H. Papadimitriou, Computational Complexity, Addison-Wesley, 1994."},{"issue":"1","key":"6_CR18","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"John Alan Robinson, A machine-oriented logic based on the resolution principle, J. ACM, 12(1) (1965) 23\u201341.","journal-title":"J. ACM"},{"key":"6_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Technical Report of the Institute of Informatics, Warsaw University","author":"A. Schubert","year":"1997","unstructured":"Aleksy Schubert, Linear interpolation for the higher order matching problem, Technical Report of the Institute of Informatics, Warsaw University, TR 96-16 (237), also in Proc. 7th Int\u2019l Joint Conf. Theory and Practice of Software Development, TAPSOFT\u201997, Lille, France, April 14-18, 1997, M. Bidoit, M. Dauchet, eds., LNCS 1214, Springer-Verlag, 1997."},{"key":"6_CR20","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","volume":"9","author":"R. Statman","year":"1979","unstructured":"Richard Statman, Intuitionistic propositional logic is polynomial-space complete, Theoret. Comput. Sci., 9 (1979) 67\u201372.","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR21","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","volume":"9","author":"R. Statman","year":"1979","unstructured":"Richard Statman, The typed \u03bb-calculus is not elementary recursive, Theoret. Comput. Sci., 9 (1979) 73\u201381.","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"6_CR22","doi-asserted-by":"publisher","first-page":"17","DOI":"10.2307\/2273377","volume":"47","author":"R. Statman","year":"1982","unstructured":"Richard Statman, Completeness, invariance and \u03bb-definability, J. Symbolic Logic, 47(1) (1982) 17\u201326.","journal-title":"J. Symbolic Logic"},{"key":"6_CR23","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(81)90086-4","volume":"15","author":"R. Statman","year":"1981","unstructured":"Richard Statman, On the existence of closed terms in the typed \u03bb-calculus II: transformations of unification problems, Theoret. Comput. Sci., 15 (1981) 329\u2013338.","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Sergei Vorobyov, The \u201cHardest\u201d Natural Decidable Theory, Proc. 12th Annual IEEE Symp. Logic in Comput. Sci., LICS\u201997, Warsaw, Poland, June 29-July 2, 1997, 294\u2013305.","DOI":"10.1109\/LICS.1997.614956"},{"key":"6_CR25","unstructured":"David A. Wolfram, The decidability of higher-order matching, Proc. 6th Int\u2019lWorkshop on Unification, Schlo\u00df Dagstuhl, Germany, July 29-31, 1992."},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"David A. Wolfram, The Clausal Theory of Types, Cambridge Tracts in Theor. Comput. Sci. vol. 36, Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511569906"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T05:54:23Z","timestamp":1737525263000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}