{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:13Z","timestamp":1725484093565},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439295"},{"type":"electronic","value":"9783540456162"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45616-3_2","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T00:26:55Z","timestamp":1179361615000},"page":"2-23","source":"Crossref","is-referenced-by-count":10,"title":["Using Linear Logic to Reason about Sequent Systems"],"prefix":"10.1007","author":[{"given":"Dale","family":"Miller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elaine","family":"Pimentel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Arnon Avron and Iddo Lev. Canonical propositional gentzen-type systems. In R. Gor\u00e9, A. Leitsch, and T. Nipkow, editors, IJCAR 2001, volume 2083 of LNAI, pages 529\u2013544. Springer-Verlag, 2001.","key":"2_CR1","DOI":"10.1007\/3-540-45744-5_45"},{"issue":"3","key":"2_CR2","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1992","unstructured":"Jean-Marc 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":"1","key":"2_CR3","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0168-0072(99)00014-7","volume":"101","author":"V. M. Abrusci","year":"1999","unstructured":"V. Michele Abrusci and Paul Ruet. Non-commutative logic I: The multiplicative fragment. Annals of Pure and Applied Logic, 101(1):29\u201364, 1999.","journal-title":"Annals of Pure and Applied Logic"},{"unstructured":"Jawahar Chirimar. Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania, February 1995.","key":"2_CR4"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"doi-asserted-by":"crossref","unstructured":"Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In Girard, Lafont, and Regnier, editors, Workshop on Linear Logic, pages 211\u2013224. London Mathematical Society Lecture Notes 222, Cambridge University Press, 1995.","key":"2_CR6","DOI":"10.1017\/CBO9780511629150.011"},{"issue":"8","key":"2_CR7","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465\u2013476, 1979.","journal-title":"Communications of the ACM"},{"unstructured":"Giorgio Delzanno and Maurizio Martelli. Objects in Forum. In Proceedings of the International Logic Programming Symposium, 1995.","key":"2_CR8"},{"issue":"3","key":"2_CR9","doi-asserted-by":"crossref","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"Roy Dyckhoff","year":"1992","unstructured":"Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57(3):795\u2013807, September 1992.","journal-title":"Journal of Symbolic Logic"},{"doi-asserted-by":"crossref","unstructured":"Amy Felty and Dale Miller. Specifying theorem provers in a higher-order logic programming language. In Ninth International Conference on Automated Deduction, pages 61\u201380, Argonne, IL, May 1988. Springer-Verlag.","key":"2_CR10","DOI":"10.1007\/BFb0012823"},{"key":"2_CR11","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gerhard Gentzen. Investigations into logical deductions. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68\u2013131. North-Holland Publishing Co., Amsterdam, 1969."},{"key":"2_CR12","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","volume":"59","author":"J.-Y. Girard","year":"1993","unstructured":"Jean-Yves Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201\u2013217, 1993.","journal-title":"Annals of Pure and Applied Logic"},{"key":"2_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-44802-0_5","volume-title":"CSL 2001","author":"A. Guglielmi","year":"2001","unstructured":"Alessio Guglielmi and Lutz Stra\u00dfburger. Non-commutativity and MELL in the calculus of structures. In L. Fribourg, editor, CSL 2001, volume 2142 of LNCS, pages 54\u201368, 2001."},{"issue":"1","key":"2_CR14","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u2013184, 1993.","journal-title":"Journal of the ACM"},{"doi-asserted-by":"crossref","unstructured":"Patrick Lincoln, Andre Scedrov, and Natarajan Shankar. Linearizing intuitionistic implication. In Annals of Pure and Applied Logic, pages 151\u2013177, 1993.","key":"2_CR15","DOI":"10.1016\/0168-0072(93)90041-B"},{"key":"2_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/3-540-56454-3_13","volume-title":"Proceedings of the 1992 Workshop on Extensions to Logic Programming","author":"D. Miller","year":"1993","unstructured":"Dale Miller. The \u03c0-calculus as a theory in linear logic: Preliminary results. In E. Lamma and P. Mello, editors, Proceedings of the 1992 Workshop on Extensions to Logic Programming, number 660 in LNCS, pages 242\u2013265. Springer-Verlag, 1993."},{"issue":"1","key":"2_CR17","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0304-3975(96)00045-X","volume":"165","author":"Dale Miller","year":"1996","unstructured":"Dale Miller. Forum: A multiple-conclusion specification language. Theoretical Computer Science, 165(1):201\u2013232, September 1996.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Dale Miller. Abstract syntax for variable binders: An overview. In John Lloyd and et. al., editors, Computational Logic-CL 2000, number 1861 in LNAI, pages 239\u2013253. Springer, 2000.","key":"2_CR18","DOI":"10.1007\/3-540-44957-4_16"},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","volume":"232","author":"R. McDowell","year":"2000","unstructured":"Raymond McDowell and Dale Miller. Cut-elimination for a logic with definitions and induction. Theoretical Computer Science, 232:91\u2013119, 2000.","journal-title":"Theoretical Computer Science"},{"key":"2_CR20","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125\u2013157, 1991.","journal-title":"Annals of Pure and Applied Logic"},{"unstructured":"Dale Miller and Elaine Pimentel. Linear logic as a framework for specifying sequent calculus. To appear in the Proceedings of Logic Colloquium 1999.","key":"2_CR21"},{"unstructured":"Gopalan Nadathur and Dale Miller. An Overview of \u03bbProlog. In Fifth International Logic Programming Conference, pages 810\u2013827, Seattle, August 1988. MIT Press.","key":"2_CR22"},{"doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363\u2013397, September 1989.","key":"2_CR23","DOI":"10.1007\/BF00248324"},{"key":"2_CR24","series-title":"PhD thesis","volume-title":"L\u00f3gica linear e a especifica\u00e7\u00e3o de sistemas computacionais","author":"E. G. Pimentel","year":"2001","unstructured":"Elaine Gouv\u00eaa Pimentel. L\u00f3gica linear e a especifica\u00e7\u00e3o de sistemas computacionais. PhD thesis, Universidade Federal de Minas Gerais, Belo Horizonte, M.G., Brasil, December 2001. (written in English)."},{"doi-asserted-by":"crossref","unstructured":"Christian Retor\u00e9. Pomset logic: a non-commutative extension of classical linear logic. In Proceedings of TLCA, volume 1210, pages 300\u2013318, 1997.","key":"2_CR25","DOI":"10.1007\/3-540-62688-3_43"},{"unstructured":"Giorgia Ricci. On the expressive powers of a Logic Programming presentation of Linear Logic (FORUM). PhD thesis, Department of Mathematics, Siena University, December 1998.","key":"2_CR26"}],"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-45616-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T13:42:20Z","timestamp":1550324540000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45616-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439295","9783540456162"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-45616-3_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}