{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214274,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651413"},{"type":"electronic","value":"9783540495451"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"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":[[1998]]},"DOI":"10.1007\/3-540-49545-2_12","type":"book-chapter","created":{"date-parts":[[2007,8,6]],"date-time":"2007-08-06T18:41:28Z","timestamp":1186425688000},"page":"169-184","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Matrix Characterization for $$ \\mathcal{M}\\mathcal{E}\\mathcal{L}\\mathcal{L} $$"],"prefix":"10.1007","author":[{"given":"Heiko","family":"Mantel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Kreitz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,2,26]]},"reference":[{"issue":"3","key":"12_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1992","unstructured":"J.-M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297\u2013347, 1992.","journal-title":"Journal of Logic and Computation"},{"issue":"2","key":"12_CR2","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. Andrews","year":"1981","unstructured":"P. Andrews. Theorem-Proving via General Matings. Jour. of the ACM 28(2), 193\u2013214, 1981.","journal-title":"Jour. of the ACM"},{"key":"12_CR3","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"W. Bibel. On matrices with connections. Jour. of the ACM 28, 633\u2013645, 1981.","journal-title":"Jour. of the ACM"},{"key":"12_CR4","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF03037438","volume":"4","author":"W. Bibel","year":"1986","unstructured":"W. Bibel. A deductive solution for plan generation. New Generation Computing 4:115\u2013132,1986.","journal-title":"New Generation Computing"},{"doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, 1987.","key":"12_CR5","DOI":"10.1007\/978-3-322-90102-6"},{"doi-asserted-by":"crossref","unstructured":"I. Cervesato, J.S. Hodas, F. Pfenning. Efficient resource management for linear logic proof search. In Extensions of Logic Programming, LNAI 1050, pages 67\u201381. Springer, 1996.","key":"12_CR6","DOI":"10.1007\/3-540-60983-0_5"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/BF01622878","volume":"28","author":"V. Danos","year":"1989","unstructured":"V. Danos & L. Regnier. The structure of the multiplicatives. Arch. Math. Logic 28:181\u2013203, 1989.","journal-title":"Arch. Math. Logic"},{"unstructured":"B. Fronh\u00f6fer. The action-as-implication paradigm. CS Press, 1996.","key":"12_CR8"},{"unstructured":"D. Galmiche. Connection methods in linear logic fragments and proof nets. Technical report, CADE-13 workshop on proof search in type-theoretic languages, 1996.","key":"12_CR9"},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0304-3975(94)00105-7","volume":"135","author":"D. Galmiche","year":"1994","unstructured":"D. Galmiche & G. Perrier. On proof normalization in linear logic. TCS, 135:67\u2013110, 1994.","journal-title":"TCS"},{"doi-asserted-by":"crossref","unstructured":"V. Gehlot and C. Gunter. Normal process representatives. Sixth Annual Symposium on Logic in Computer Science, pages 200\u2013207, 1991.","key":"12_CR11","DOI":"10.1109\/LICS.1990.113746"},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"J.-Y. Girard. Linear logic. TCS, 50:1\u2013102, 1987.","journal-title":"TCS"},{"key":"12_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/3-540-63104-6_21","volume-title":"14 th Conference on Automated Deduction","author":"J. Harland","year":"1997","unstructured":"J. Harland and D. Pym. Resource-Distribution via Boolean Constraints. 14 th Conference on Automated Deduction, LNCS 1249, pp. 222\u2013236. Springer, 1997."},{"issue":"2","key":"12_CR14","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1006\/inco.1994.1036","volume":"110","author":"J.S. Hodas","year":"1994","unstructured":"J.S. Hodas & D. Miller. Logic programming in a fragment of linear logic. Journal of Information and Computation, 110(2):327\u2013365, 1994.","journal-title":"Journal of Information and Computation"},{"key":"12_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/3-540-63104-6_20","volume-title":"14 th Conference on Automated Deduction","author":"C. Kreitz","year":"1997","unstructured":"C. Kreitz, H. Mantel, J. Otten, S. Schmitt. Connection-Based Proof Construction in Linear Logic. 14 th Conference on Automated Deduction, LNCS 1249, pp. 207\u2013221. Springer, 1997."},{"key":"12_CR16","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0304-3975(94)00108-1","volume":"135","author":"P. Lincoln","year":"1994","unstructured":"P. Lincoln and T. Winkler. Constant-only multiplicative linear logic is NP-complete. TCS, 135:155\u2013169, 1994.","journal-title":"TCS"},{"doi-asserted-by":"crossref","unstructured":"H. Mantel. Developing a Matrix Characterization for $$ \\mathcal{M}\\mathcal{E}\\mathcal{L}\\mathcal{L} $$ . Technical Report, DFKI Saarbr\u00fccken, 1998. http:\/\/www.dfki.de\/vse\/staff\/mantel\/Papers\/98tr-dev-mc-mell.ps.gz","key":"12_CR17","DOI":"10.1007\/3-540-49545-2_12"},{"key":"12_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"M. Masseron","year":"1991","unstructured":"M. Masseron, C. Tollu, J. Vauzeilles. Generating plans in linear logic. In Foundations of Software Technology and Theoretical Computer Science, LNCS, Springer, 1991."},{"issue":"1","key":"12_CR19","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0304-3975(96)00045-X","volume":"165","author":"D. Miller","year":"1996","unstructured":"D. Miller. FORUM: A Multiple-Conclusion Specification Logic. TCS, 165(1):201\u2013232, 1996.","journal-title":"TCS"},{"doi-asserted-by":"crossref","unstructured":"J. Otten & C. Kreitz. A Uniform Proof Procedure for Classical and Non-classical Logics. KI-96: Advances in Artificial Intelligence, LNAI 1137, pp. 307\u2013319. Springer, 1996.","key":"12_CR20","DOI":"10.1007\/3-540-61708-6_70"},{"doi-asserted-by":"crossref","unstructured":"S. Schmitt, C. Kreitz. Converting non-classical matrix proofs into sequent-style systems. CADE-13, LNAI 1104, pp. 418\u2013432, Springer, 1996.","key":"12_CR21","DOI":"10.1007\/3-540-61511-3_104"},{"unstructured":"S. Schmitt, C. Kreitz. A uniform procedure for converting non-classical matrix proofs into sequent-style systems. Journal of Information and Computation, submitted.","key":"12_CR22"},{"key":"12_CR23","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/BF00885763","volume":"12","author":"T. Tammet","year":"1994","unstructured":"T. Tammet. Proof strategies in linear logic. Jour. of Automated Reasoning, 12:273\u2013304, 1994.","journal-title":"Jour. of Automated Reasoning"},{"unstructured":"L. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990.","key":"12_CR24"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49545-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T04:40:12Z","timestamp":1737348012000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49545-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651413","9783540495451"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-49545-2_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"26 February 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}