{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:25:09Z","timestamp":1743139509008,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230243"},{"type":"electronic","value":"9783540301240"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30124-0_19","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T12:27:59Z","timestamp":1267532879000},"page":"220-234","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Higher-Order Matching in the Linear \u03bb-calculus with Pairing"],"prefix":"10.1007","author":[{"given":"Philippe","family":"de Groote","sequence":"first","affiliation":[]},{"given":"Sylvain","family":"Salvati","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,9,9]]},"reference":[{"issue":"4","key":"19_CR1","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1006\/jsco.1997.0185","volume":"25","author":"H. Comon","year":"1998","unstructured":"Comon, H.: Completion of rewrite systems with membership constraints. Part I: Deduction rules. Journal of Symbolic Computation\u00a025(4), 397\u2013419 (1998)","journal-title":"Journal of Symbolic Computation"},{"issue":"4","key":"19_CR2","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1006\/jsco.1997.0186","volume":"25","author":"H. Comon","year":"1998","unstructured":"Comon, H.: Completion of rewrite systems with membership constraints. Part II: Constraint solving. Journal of Symbolic Computation\u00a025(4), 421\u2013453 (1998)","journal-title":"Journal of Symbolic Computation"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem proving procedures. In: Proceedings of the 3rd annual ACM Symposium on Theory of Computing, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"key":"19_CR4","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)"},{"issue":"2\u20133","key":"19_CR5","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0168-0072(94)90083-3","volume":"69","author":"G. Dowek","year":"1994","unstructured":"Dowek, G.: Third order matching is decidable. Annals of Pure and Applied Logic\u00a069(2\u20133), 135\u2013155 (1994)","journal-title":"Annals of Pure and Applied Logic"},{"key":"19_CR6","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, pp. 1009\u20131062. Elsevier, Amsterdam (2001)"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.Y. Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoritical Computer Science\u00a050, 1\u2013102 (1987)","journal-title":"Theoritical Computer Science"},{"issue":"2","key":"19_CR8","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W.D. Goldfarb","year":"1981","unstructured":"Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoretical Computer Science\u00a013(2), 225\u2013230 (1981)","journal-title":"Theoretical Computer Science"},{"key":"19_CR9","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.h.: Higher-order linear matching is NP-complete. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 127\u2013140. Springer, Heidelberg (2000)"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-44881-0_17","volume-title":"Rewriting Techniques and Applications","author":"P. Groote de","year":"2003","unstructured":"de Groote, P.h., Salvati, S.: On the complexity of higher-order matching in the linear. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 234\u2013245. Springer, Heidelberg (2003)"},{"issue":"3","key":"19_CR11","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"G. Huet","year":"1973","unstructured":"Huet, G.: The undecidability of unification in third order logic. Information and Control\u00a022(3), 257\u2013267 (1973)","journal-title":"Information and Control"},{"key":"19_CR12","unstructured":"Huet, G.: R\u00b4esolution d\u2019\u00b4equations dans les langages d\u2019ordre 1, 2,..., \u03c9. Th\u00e8se de Doctorat d\u2019Etat, Universit\u00e9 Paris 7 (1976)"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/3-540-61464-8_63","volume-title":"Rewriting Techniques and Applications","author":"J. Levy","year":"1996","unstructured":"Levy, J.: Linear second-order unification. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, pp. 332\u2013346. Springer, Heidelberg (1996)"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1093\/jigpal\/11.1.51","volume":"11","author":"R. Loader","year":"2002","unstructured":"Loader, R.: Higher order \u03b2 matching is undecidable. Logic Journal of the IGPL\u00a011(1), 51\u201368 (2002)","journal-title":"Logic Journal of the IGPL"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-540-45208-9_4","volume-title":"Theoretical Computer Science","author":"H. Mairson","year":"2003","unstructured":"Mairson, H., Terui, K.: On the Computational Complexity of Cut-Elimination in Linear Logic. In: Blundo, C., Laneve, C. (eds.) ICTCS 2003. LNCS, vol.\u00a02841, pp. 23\u201336. Springer, Heidelberg (2003)"},{"key":"19_CR16","unstructured":"Padovani, V.: Filtrage d\u2019ordre sup\u00b4erieure. Th\u00e8se de Doctorat, Universit\u00e9 de Paris 7 (1996)"},{"key":"19_CR17","unstructured":"Schmidt-Schau\u00df, M., Stuber, J.: On the complexity of linear and stratified context matching problems. Rapport de recherche A01-R-411, LORIA (December 2001)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30124-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T20:03:44Z","timestamp":1579723424000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30124-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230243","9783540301240"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30124-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]},"assertion":[{"value":"9 September 2004","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}