{"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":1775818978292,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540660866","type":"print"},{"value":"9783540487548","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48754-9_20","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:20:56Z","timestamp":1184602856000},"page":"217-231","source":"Crossref","is-referenced-by-count":11,"title":["linTAP : A Tableau Prover for Linear Logic"],"prefix":"10.1007","author":[{"given":"Heiko","family":"Mantel","sequence":"first","affiliation":[]},{"given":"Jens","family":"Otten","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,11]]},"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":"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"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"B. Beckert, J. Posegga. lean TAP: Lean Tableau-Based Theorem Proving. 12 th Conference on Automated Deduction, LNAI 814, pp. 793\u2013797. Springer, 1994.","DOI":"10.1007\/3-540-58156-1_62"},{"issue":"3","key":"20_CR3","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"B. Beckert","year":"1995","unstructured":"B. Beckert, J. Posegga. leanTAP: Lean Tableau-Based Deduction. Journal of Automated Reasoning, 15(3), pp. 339\u2013358, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"B. Beckert, R. Gor\u00e9. Free Variable Tableaux for Propositional Modal Logics. Proc. 6 th TABLEAUX Conference, LNAI 1227, pp. 91\u2013106, Springer 1997.","DOI":"10.1007\/BFb0027407"},{"key":"20_CR5","unstructured":"W. Bibel. Let\u2019s plan it deductively!. In IJCAI-97, Morgan Kaufmann, 1997."},{"key":"20_CR6","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.","DOI":"10.1007\/3-540-60983-0_5"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"M. Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1996.","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"20_CR8","unstructured":"B. Fronh\u00f6fer. The action-as-implication paradigm. CS Press, 1996."},{"key":"20_CR9","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":"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 and C. Gunter. Normal process representatives. Sixth Annual Symposium on Logic in Computer Science, pages 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. TCS, 50:1\u2013102, 1987.","journal-title":"TCS"},{"key":"20_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":"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","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":"20_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"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"H. Mantel, C. Kreitz. A Matrix Characterization for MELL. Logics in Artificial Intelligence, JELIA\u2019 98, LNAI 1489, pp. 169\u2013183, Springer, 1998.","DOI":"10.1007\/3-540-49545-2_12"},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari. An efficient unification algorithm. ACM TOPLAS, 4:258\u2013282, 1982.","journal-title":"ACM TOPLAS"},{"key":"20_CR19","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":"20_CR20","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"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"J. Otten. ileanTAP: An Intuitionistic Theorem Prover. Proc. 6 th TABLEAUX Conference, LNAI 1227, pp. 307\u2013312, Springer 1997.","DOI":"10.1007\/BFb0027422"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"J. Otten, C. Kreitz. T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods. Proc. 5 th TABLEAUX Workshop, LNAI 1071, pp. 244\u2013260, 1996.","DOI":"10.1007\/3-540-61208-4_16"},{"key":"20_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. JAR, 12:273\u2013304, 1994.","journal-title":"JAR"},{"key":"20_CR24","volume-title":"User\u2019s Guide of a Linear Logic Theorem Prover (llprover)","author":"N. Tamura","year":"1995","unstructured":"N. Tamura. User\u2019s Guide of a Linear Logic Theorem Prover (llprover). Technical report. Faculty of Engineering, Kobe University, Japan, 1995."},{"key":"20_CR25","unstructured":"L. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48754-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T11:54:17Z","timestamp":1737287657000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48754-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660866","9783540487548"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-48754-9_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}