{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T01:12:43Z","timestamp":1742951563768,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540637004"},{"type":"electronic","value":"9783540696315"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0052164","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T04:43:12Z","timestamp":1149655392000},"page":"310-328","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Generation as deduction on labelled proof nets"],"prefix":"10.1007","author":[{"given":"Josep M.","family":"Merenciano","sequence":"first","affiliation":[]},{"given":"Glyn","family":"Morrill","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,16]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/BF01622878","volume":"28","author":"V. Danos","year":"1989","unstructured":"V. Danos and L. Regnier. The structure of multiplicatives. Archive for mathematical logic, (28):181\u2013203, 1989.","journal-title":"Archive for mathematical logic"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Gilles Dowek. Third order matching is decidable. In 7th Annual IEEE Symposium of Logic in Computer Science, pages 2\u201310, 1992.","DOI":"10.1109\/LICS.1992.185514"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Dov Gabbay. Labelled Deductive Systems. Oxford University Press, 1996.","DOI":"10.1093\/oso\/9780198538332.001.0001"},{"key":"17_CR4","volume-title":"Designing unification procedures using transformations: a survey","author":"J. Gallier","year":"1989","unstructured":"Jean Gallier and Wayne Snyder. Designing unification procedures using transformations: a survey. In Workshop Logic For Computer Science. MSRI Berkeley, 1989."},{"issue":"1","key":"17_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J. Girard","year":"1987","unstructured":"Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1\u2013102, 1987.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"17_CR6","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W. Goldfard","year":"1981","unstructured":"W. Goldfard. The undecibility of the second-order unification problem. Theoretical Computer Science, 13(2):225\u2013230, 1981.","journal-title":"Theoretical Computer Science"},{"key":"17_CR7","unstructured":"G. Huet. Constrained Resolution: A Complete Method for Higher-Order Logic. PhD thesis, Case Western Reserve University, 1972."},{"issue":"1","key":"17_CR8","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(1):27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"17_CR9","doi-asserted-by":"publisher","first-page":"154","DOI":"10.2307\/2310058","volume":"65","author":"J. Lambek","year":"1958","unstructured":"J. Lambek. The mathematics of sentence structure. American Mathematical Monthly, (65): 154\u2013170, 1958.","journal-title":"American Mathematical Monthly"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Jordi Levy. Linear second-order unification. Rewriting Techniques and Applications, 1996.","DOI":"10.1007\/3-540-61464-8_63"},{"key":"17_CR11","unstructured":"Xavier Llor\u00e9 and Glyn Morrill. Difference lists and difference bags for logic programming of categorial deduction. In Proceedings of the Sociedad Espanola para el Procesamiento del Lenguaje Natural, pages 115\u2013129, 1995."},{"key":"17_CR12","first-page":"403","volume-title":"Proceedings Eight Amsterdam Colloquium","author":"M. Moortgat","year":"1992","unstructured":"Michael Moortgat. Labelled deductive systems for categorial theorem proving. In Proceedings Eight Amsterdam Colloquium, pages 403\u2013424, Amsterdam, 1992. Institute of Language, Logic and Information, Universiteit van Amsterdam."},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Glyn Morrill. Type Logical Grammar: Categorial Logic of Signs. Kluwer Academic Publishers, 1994.","DOI":"10.1007\/978-94-011-1042-6"},{"issue":"2\u20133","key":"17_CR14","first-page":"403","volume":"3","author":"G. Morrill","year":"1995","unstructured":"Glyn Morrill. Clausal proofs and discontinuity. Bulletin of the Interest Group in Pure and Applied Logics, 3(2\u20133):403\u2013427, 1995.","journal-title":"Bulletin of the Interest Group in Pure and Applied Logics"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Glyn Morrill. Higher-order linear logic programming of categorial deduction. In Proceedings ACL, pages 133\u2013140, 1995.","DOI":"10.3115\/976973.976993"},{"key":"17_CR16","unstructured":"Glyn Morrill. Memoisation of categorial proof nets: parallelism in categorial processing. In Michele Abrusci and Claudia Casadio, editors, Proof and Linguistic Categories: Proceedings 1996 Roma Workshop, pages 157\u2013169. Universit\u00e0 di Bologna, 1996. To appear in S. Manandhar, W. Nutt and G. Lopez (eds.), Springer-Verlag."},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"F. Pereira and D. Warren. Parsing as deduction. In Proceedings ACL, pages 132\u2013144, 1983.","DOI":"10.3115\/981311.981338"},{"key":"17_CR18","unstructured":"Dirk Roorda. Resource Logics: Proof-theoretical Investigations. PhD thesis, Universiteit van Amsterdam, 1991."},{"key":"17_CR19","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W. Snyder","year":"1989","unstructured":"Wayne Snyder and Jean Gallier. Higher-order unification revisited: Complete sets of transformations. Journal of Symbolic Computation, (8): 101\u2013140, 1989.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Logical Aspects of Computational Linguistics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0052164","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T07:04:26Z","timestamp":1736406266000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0052164"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540637004","9783540696315"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0052164","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"16 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}