{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T11:02:58Z","timestamp":1775818978130,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631040","type":"print"},{"value":"9783540691402","type":"electronic"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"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":[[1997]]},"DOI":"10.1007\/3-540-63104-6_20","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:04:42Z","timestamp":1330297482000},"page":"207-221","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Connection-based proof construction in linear logic"],"prefix":"10.1007","author":[{"given":"C.","family":"Kreitz","sequence":"first","affiliation":[]},{"given":"H.","family":"Mantel","sequence":"additional","affiliation":[]},{"given":"J.","family":"Otten","sequence":"additional","affiliation":[]},{"given":"S.","family":"Schmitt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"issue":"3","key":"20_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1993","unstructured":"J.-M. Andreoli. Logic programming with focussing proofs in linear logic. Journal of Logic and Computation, 2(3):297\u2013347, 1993.","journal-title":"Journal of Logic and Computation"},{"key":"20_CR2","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. Journal of the ACM, 28:633\u2013645, 1981.","journal-title":"Journal of the ACM"},{"key":"20_CR3","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"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated theorem proving. Vieweg, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"20_CR5","first-page":"67","volume":"1050","author":"I. Cervesato","year":"1996","unstructured":"I. Cervesato, J.S. Hodas, F. Pfenning Efficient resource management for linear logic proof search. Extensions of Logic Programming, LNAI 1050, pp. 67\u201381, 1996.","journal-title":"LNAI"},{"key":"20_CR6","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. Archive for Mathematical Logic, 28:181\u2013203, 1989.","journal-title":"Archive for Mathematical Logic"},{"key":"20_CR7","unstructured":"B. Fronh\u00f6fer The action-as-implication paradigm, CS Press, 1996."},{"key":"20_CR8","unstructured":"D. Galmiche Connection methods in linear logic fragments and proof nets construction. CADE-13 workshop on proof search in type-theoretic languages, 1996."},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"D. Galmiche, G. Perrier. A procedure for automatic proof nets construction. LPAR'92, LNAI 624, pp. 42\u201353, Springer Verlag, 1992.","DOI":"10.1007\/BFb0013047"},{"key":"20_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"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"V. Gehlot, C. Gunter. Normal process representatives. In Proc. 5-th Annual IEEE Symposium on Logic in Computer Science, pp. 200\u2013207, 1991.","DOI":"10.1109\/LICS.1990.113746"},{"key":"20_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. Theoretical Computer Science, 50:1\u2013102, 1987.","journal-title":"Theoretical Computer Science"},{"key":"20_CR13","first-page":"97","volume":"150","author":"J.-Y. Girard","year":"1996","unstructured":"J.-Y. Girard. Proof-nets: the parallel syntax for proof-theory. In Logic and Algebra, LNPAM 150, pp. 97\u2013124, 1996.","journal-title":"LNPAM"},{"issue":"2","key":"20_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":"20_CR15","volume-title":"Diplomarbeit","author":"H. Mantel","year":"1996","unstructured":"H. Mantel. Eine Matrixcharakterisierung f\u00fcr ein Fragment der linearen Logik. Diplomarbeit, TH-Darmstadt, Germany, 1996."},{"key":"20_CR16","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli, U. Montanari. An efficient unification algorithm. ACM TOPLAS, 4:258\u2013282, 1982.","journal-title":"ACM TOPLAS"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"M. Masseron, C. Tollu, J. Vauzielles Generating plans in linar logic. In Foundations of Software Technology and Theoretical Computer Science, LNCS 472, pp. 63\u201375, Springer, 1990.","DOI":"10.1007\/3-540-53487-3_35"},{"key":"20_CR18","first-page":"463","volume":"4","author":"J. McCarthy","year":"1969","unstructured":"J. McCarthy, P.H. Hayes Some philosophical problems from the standpoint of Artificial Intelligence Machine Intelligence, 4:463\u2013502, 1969.","journal-title":"Machine Intelligence"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"J. Otten, C. Kreitz. A connection based proof method for intuitionistic logic. 4 th TABLEAUX Workshop, LNAI 918, pp. 122\u2013137, Springer Verlag, 1995.","DOI":"10.1007\/3-540-59338-1_32"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"J. Otten, C. Kreitz. T-string-unification: unifying prefixes in non-classical proof methods. 5 th TABLEAUX Workshop, LNAI 1071, pp. 244\u2013260, Springer Verlag, 1996.","DOI":"10.1007\/3-540-61208-4_16"},{"key":"20_CR21","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 Verlag, 1996.","DOI":"10.1007\/3-540-61708-6_70"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"J. Otten. ileanTAP: An intuitionistic theorem prover. International Conference TABLEAUX'97, LNAI, Springer Verlag, 1997.","DOI":"10.1007\/BFb0027422"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"S. Schmitt, C. Kreitz. On transforming intuitionistic matrix proofs into standard-sequent proofs. 4 th TABLEAUX Workshop, LNAI 918, pp. 106\u2013121, Springer Verlag, 1995.","DOI":"10.1007\/3-540-59338-1_31"},{"key":"20_CR24","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 Verlag, 1996.","DOI":"10.1007\/3-540-61511-3_104"},{"key":"20_CR25","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":"20_CR26","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"},{"key":"20_CR27","unstructured":"L. Wallen. Automated deduction in non-classical logics. MIT Press, 1990."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-14"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63104-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:36:32Z","timestamp":1742600192000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}