Abstract
Linear logic can be used as a meta-logic for the specification of some sequent calculus proof systems. We explore in this paper properties of such linear logic specifications. We show that derivability of one proof system from another has a simple decision procedure that is implemented simply via bounded logic programming search. We also provide conditions to ensure that an encoded proof system has the cut-elimination property and show that this can be decided again by simple, bounded proof search algorithms.
Miller has been supported in part by NSF grants CCR-9912387, CCR-9803971, INT-9815645, and INT-9815731. Both authors wish to thank L’Institut de Mathématiques de Luminy, University Aix-Marseille 2 for the support to attend the Logic and Interaction Weeks in February 2002, during which much of this paper was written.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arnon Avron and Iddo Lev. Canonical propositional gentzen-type systems. In R. Goré, A. Leitsch, and T. Nipkow, editors, IJCAR 2001, volume 2083 of LNAI, pages 529–544. Springer-Verlag, 2001.
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992.
V. Michele Abrusci and Paul Ruet. Non-commutative logic I: The multiplicative fragment. Annals of Pure and Applied Logic, 101(1):29–64, 1999.
Jawahar Chirimar. Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania, February 1995.
Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.
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–224. London Mathematical Society Lecture Notes 222, Cambridge University Press, 1995.
Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, 1979.
Giorgio Delzanno and Maurizio Martelli. Objects in Forum. In Proceedings of the International Logic Programming Symposium, 1995.
Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57(3):795–807, September 1992.
Amy Felty and Dale Miller. Specifying theorem provers in a higher-order logic programming language. In Ninth International Conference on Automated Deduction, pages 61–80, Argonne, IL, May 1988. Springer-Verlag.
Gerhard Gentzen. Investigations into logical deductions. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68–131. North-Holland Publishing Co., Amsterdam, 1969.
Jean-Yves Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201–217, 1993.
Alessio Guglielmi and Lutz Straßburger. Non-commutativity and MELL in the calculus of structures. In L. Fribourg, editor, CSL 2001, volume 2142 of LNCS, pages 54–68, 2001.
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, 1993.
Patrick Lincoln, Andre Scedrov, and Natarajan Shankar. Linearizing intuitionistic implication. In Annals of Pure and Applied Logic, pages 151–177, 1993.
Dale Miller. The π-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–265. Springer-Verlag, 1993.
Dale Miller. Forum: A multiple-conclusion specification language. Theoretical Computer Science, 165(1):201–232, September 1996.
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–253. Springer, 2000.
Raymond McDowell and Dale Miller. Cut-elimination for a logic with definitions and induction. Theoretical Computer Science, 232:91–119, 2000.
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–157, 1991.
Dale Miller and Elaine Pimentel. Linear logic as a framework for specifying sequent calculus. To appear in the Proceedings of Logic Colloquium 1999.
Gopalan Nadathur and Dale Miller. An Overview of λProlog. In Fifth International Logic Programming Conference, pages 810–827, Seattle, August 1988. MIT Press.
Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–397, September 1989.
Elaine Gouvêa Pimentel. Lógica linear e a especificação de sistemas computacionais. PhD thesis, Universidade Federal de Minas Gerais, Belo Horizonte, M.G., Brasil, December 2001. (written in English).
Christian Retoré. Pomset logic: a non-commutative extension of classical linear logic. In Proceedings of TLCA, volume 1210, pages 300–318, 1997.
Giorgia Ricci. On the expressive powers of a Logic Programming presentation of Linear Logic (FORUM). PhD thesis, Department of Mathematics, Siena University, December 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miller, D., Pimentel, E. (2002). Using Linear Logic to Reason about Sequent Systems. In: Egly, U., Fermüller, C.G. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2002. Lecture Notes in Computer Science(), vol 2381. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45616-3_2
Download citation
DOI: https://doi.org/10.1007/3-540-45616-3_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43929-5
Online ISBN: 978-3-540-45616-2
eBook Packages: Springer Book Archive