{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:29:36Z","timestamp":1725568176597},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_41","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T09:13:30Z","timestamp":1288084410000},"page":"488-502","source":"Crossref","is-referenced-by-count":3,"title":["Decidability of Arity-Bounded Higher-Order Matching"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"41_CR1","volume-title":"The Lambda Calculus. Its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus. Its Syntax and Semantics. North- Holland, Amsterdam (1984)"},{"key":"41_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/BFb0028013","volume-title":"Computer Science Logic","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Higher-order matching and tree automata. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol.\u00a01414, pp. 157\u2013176. Springer, Heidelberg (1998)"},{"key":"41_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/10721975_9","volume-title":"Rewriting Techniques and Applications","author":"P. Groote de","year":"2000","unstructured":"de Groote, P.: Linear higher-order matching is NP-complete. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 127\u2013140. Springer, Heidelberg (2000)"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"Dowek, G.: Third order matching is decidable. In: Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science, pp. 2\u201310 (1992)","DOI":"10.1109\/LICS.1992.185514"},{"key":"41_CR5","doi-asserted-by":"publisher","first-page":"1009","DOI":"10.1016\/B978-044450813-3\/50018-7","volume-title":"Handbook of Automated Reasoning","author":"G. Dowek","year":"2001","unstructured":"Dowek, G.: Higher-order unification and matching. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02, ch. 16, pp. 1009\u20131062. North-Holland, Amsterdam (2001)"},{"key":"41_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/3-540-45610-4_24","volume-title":"Rewriting Techniques and Applications","author":"D. Dougherty","year":"2002","unstructured":"Dougherty, D., Wierzbicki, T.: A decidable variant of higher order matching. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 340\u2013351. Springer, Heidelberg (2002)"},{"key":"41_CR7","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"Huet, G.: A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science\u00a01, 27\u201357 (1975)","journal-title":"Theoretical Computer Science"},{"key":"41_CR8","unstructured":"Huet, G.: R\u00e9solution d\u2019\u00e9quations dans des langages d\u2019ordre 1,2,. . .\u03c9. Th\u00e8se de doctorat d\u2018etat, Universit\u00e9 Paris VII (1976) (in French)"},{"key":"41_CR9","unstructured":"Loader, R.: An algorithm for the minimal model. Technical report, 4 pages (1997), available on www"},{"key":"41_CR10","unstructured":"Loader, R.: Higher-order \u03b2 matching is undecidable (2001) (draft)"},{"issue":"4","key":"41_CR11","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables and simple unification. J. of Logic and Computation\u00a01(4), 497\u2013536 (1991)","journal-title":"J. of Logic and Computation"},{"key":"41_CR12","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Proc. 6th IEEE Symp. LICS, pp. 342\u2013349 (1991)","DOI":"10.1109\/LICS.1991.151658"},{"key":"41_CR13","series-title":"Applied Logic Series","first-page":"399","volume-title":"Automated Deduction \u2014 A Basis for Applications. Volume I: Foundations","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T., Prehofer, C.: Higher-order rewriting and equational reasoning. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction \u2014 A Basis for Applications. Volume I: Foundations. Applied Logic Series, vol.\u00a08, pp. 399\u2013430. Kluwer, Dordrecht (1998)"},{"key":"41_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/BFb0014063","volume-title":"Typed Lambda Calculi and Applications","author":"V. Padovani","year":"1995","unstructured":"Padovani, V.: On equivalence classes of interpolation equations. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 335\u2013349. Springer, Heidelberg (1995)"},{"key":"41_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/3-540-61780-9_71","volume-title":"Types for Proofs and Programs","author":"V. Padovani","year":"1996","unstructured":"Padovani, V.: Decidability of all minimal models. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 201\u2013215. Springer, Heidelberg (1996)"},{"issue":"3","key":"41_CR16","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1017\/S0960129500003108","volume":"10","author":"V. Padovani","year":"2000","unstructured":"Padovani, V.: Decidability of fourth-order matching. Mathematical Structures in Computer Science\u00a010(3), 361\u2013372 (2000)","journal-title":"Mathematical Structures in Computer Science"},{"key":"41_CR17","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.1016\/B978-044450813-3\/50019-9","volume-title":"Handbook of Automated Reasoning","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02, ch. 17, pp. 1063\u20131147. North-Holland, Amsterdam (2001)"},{"key":"41_CR18","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","volume":"9","author":"R. Statman","year":"1979","unstructured":"Statman, R.: The typed \u03bb-calculus is not elementary recursive. Theoretical Computer Science\u00a09, 73\u201381 (1979)","journal-title":"Theoretical Computer Science"},{"key":"41_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-48660-7_6","volume-title":"Automated Deduction - CADE-16","author":"T. Wierzbicki","year":"1999","unstructured":"Wierzbicki, T.: Complexity of the higher-order matching. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 82\u201396. Springer, Heidelberg (1999)"},{"key":"41_CR20","series-title":"Cambridge tracts in theoretical computer science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569906","volume-title":"The clausal theories of types","author":"D.A. Wolfram","year":"1993","unstructured":"Wolfram, D.A.: The clausal theories of types. Cambridge tracts in theoretical computer science, vol.\u00a021. Cambridge University Press, Cambridge (1993)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T17:32:01Z","timestamp":1553189521000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}