{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:05:39Z","timestamp":1737435939946,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439165"},{"type":"electronic","value":"9783540456100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45610-4_24","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T06:47:11Z","timestamp":1186901231000},"page":"340-351","source":"Crossref","is-referenced-by-count":8,"title":["A Decidable Variant of Higher Order Matching"],"prefix":"10.1007","author":[{"given":"Dan","family":"Dougherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ToMasz","family":"Wierzbicki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"24_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/BFb0028013","volume-title":"Proc. 11th Int\u2019l Workshop Computer Science Logic","author":"H. Comon","year":"1997","unstructured":"Hubert Comon, Yan Jurski, Higher-Order Matching and Tree Automata, Proc. 11th Int\u2019l Workshop Computer Science Logic, CSL\u201997, Mogens Nielsen, Wolfgang Thomas, eds., Aarhus, Denmark, August 1997, LNCS 1414, Springer-Verlag, 1998, 157\u2013176."},{"issue":"22","key":"24_CR2","first-page":"465","volume":"6","author":"N. Dershowitz","year":"1979","unstructured":"Nachum Dershowitz, Zohar Manna, Proving termination with multiset orderings, Comm. Assoc. for Computing Machinery, 6(22), 465\u2013476, 1979.","journal-title":"Comm. Assoc. for Computing Machinery"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Giles Dowek, Third order matching is decidable, Proc. 7th IEEE Symp. Logic in Computer Science, LICS\u201992, IEEE Press, 1992, 2\u201310, also in Annals of Pure and Applied Logic, 69, 1994, 135\u2013155.","DOI":"10.1016\/0168-0072(94)90083-3"},{"key":"24_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/10721975_9","volume-title":"Proc. 11th Int\u2019l Conf. Rewriting Techniques and Applications","author":"P. Groote de","year":"2000","unstructured":"Philippe de Groote, Linear Higher-Order Matching Is NP-Complete, Proc. 11th Int\u2019l Conf. Rewriting Techniques and Applications, RTA 2000, Leo Bachmair, ed., Norwich, UK, July 10\u201312, 2000, LNCS 1833, Springer-Verlag, 2000, 127\u2013140."},{"key":"24_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-61464-8_63","volume-title":"Proc. 7th Int\u2019l Conf. Rewriting Techniques and Applications","author":"J. Levy","year":"1996","unstructured":"Jordi Levy, Linear Second Order Unification, Proc. 7th Int\u2019l Conf. Rewriting Techniques and Applications, RTA\u201996, H. Ganzinger, ed., New Brunswick, NJ, 1996, LNCS 1103, Springer-Verlag, 1996, 332\u2013346."},{"key":"24_CR6","unstructured":"Ralph Loader, Higher Order \u03b2 Matching is Undecidable, October 2001, manuscript."},{"key":"24_CR7","doi-asserted-by":"publisher","first-page":"213","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, Theoretical Computer Science, 103, 1992, 213\u2013226.","journal-title":"Theoretical Computer Science"},{"key":"24_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/3-540-61780-9_71","volume-title":"Proc. 3rd Int\u2019l Workshop Types for Proofs and Programs","author":"V. Padovani","year":"1996","unstructured":"Vincent Padovani, Decidability of All Minimal Models, Proc. 3rd Int\u2019l Workshop Types for Proofs and Programs, TYPES\u201995, Stefano Berardi, Mario Coppo, eds., Torino, Italy, 1995, LNCS 1158, Springer-Verlag, 1996, 201\u2013215."},{"key":"24_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/BFb0014063","volume-title":"Proc.Int\u2019l Conf. Typed Lambda Calculi and Applications","author":"V. Padovani","year":"1995","unstructured":"Vincent Padovani, On equivalence classes of interpolation equations, Proc.Int\u2019l Conf. Typed Lambda Calculi and Applications, TLCA\u201995, M. Dezani-Ciancaglini, G. Plotkin, eds., LNCS 902, Springer-Verlag, 1995, 335\u2013349."},{"issue":"10","key":"24_CR10","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1017\/S0960129500003108","volume":"3","author":"V. Padovani","year":"2000","unstructured":"Vincent Padovani, Decidability of fourth-order matching, Mathematical Structures in Computer Science, 3(10), 2000, 361\u2013372.","journal-title":"Mathematical Structures in Computer Science"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Manfred Schmidt-Schau\u00df, Klaus U. Schulz, Decidability of bounded higher order unification, technical report Frank-report-15, Institut f\u00fcr Informatik, J. W. Goethe-Universit\u00e4t, Frankfurt am Main, 2001.","DOI":"10.1007\/3-540-45793-3_35"},{"key":"24_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030617","volume-title":"Proc. 7th Int\u2019l Joint Conf. Theory and Practice of Software Development","author":"A. Schubert","year":"1997","unstructured":"Aleksy Schubert, Linear interpolation for the higher order matching problem, Proc. 7th Int\u2019l Joint Conf. Theory and Practice of Software Development, TAP-SOFT\u201997, M. Bidoit, M. Dauchet, eds., LNCS 1214, Springer-Verlag, 1997."},{"key":"24_CR13","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(81)90086-4","volume":"15","author":"R. Statman","year":"1981","unstructured":"Richard Statman, The Typed \u03bb-Calculus is Not Elementary Recursive, Theoretical Computer Science, 15, 1981, 73\u201381.","journal-title":"Theoretical Computer Science"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Sergei Vorobyov, The \u201cHardest\u201d Natural Decidable Theory, Proc. 12th Annual IEEE Symp. Logic in Computer Science, LICS\u201997, IEEE Press, 1997, 294\u2013305.","DOI":"10.1109\/LICS.1997.614956"}],"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-45610-4_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T08:50:01Z","timestamp":1737363001000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45610-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439165","9783540456100"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45610-4_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}