Document Open Access Logo

Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus

Author Ryuta Arisaka

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2016.8.pdf
  • Filesize: 0.55 MB
  • 18 pages

Document Identifiers

Subject Classification

Keywords
  • cut-elimination
  • contraction-free
  • sequent calculus
  • proof theory
  • BI
  • logic combination

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Development of a contraction-free BI sequent calculus, be the
contraction-freeness implicit or explicit, has not been successful in
the literature. We address this problem by presenting such a sequent
system. Our calculus involves no structural rules. It should be an
insight into non-formula contraction absorption in other non-classical
logics. Contraction absorption in sequent calculus is associated to
simpler cut elimination and to efficient proof searches.

Cite As Get BibTex

Ryuta Arisaka. Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSCD.2016.8

Author Details

Ryuta Arisaka

References

  1. Ryuta Arisaka, Anupam Das, and Lutz Straßburger. On Nested Sequents for Constructive Modal Logics. Logical Methods in Computer Science, 11(3), 2015. Google Scholar
  2. Ryuta Arisaka and Shengchao Qin. LBI cut elimination proof with BI-Multi-Cut. In TASE, pages 235-238, 2012. Google Scholar
  3. Nuel Belnap. Display logic. Journal of Philosophical Logic, 11(4):375-417, 1982. Google Scholar
  4. James Brotherston and Cristiano Calcagno. Classical BI: a logic for reasoning about dualising resources. In POPL, pages 328-339, 2009. Google Scholar
  5. Carlos Caleiro and Jaime Ramos. Combining classical and intuitionistic implications. In Frontiers of Combining Systms, pages 118-132, 2007. Google Scholar
  6. Luis Fariñas del Cerro and Andreas Herzig. Combining classical and intuitionistic logic, or: Intuitionistic implication as a conditional. In Frontiers of Combining Systms, pages 93-102, 1996. Google Scholar
  7. Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Stephen Magill, and Sungwoo Park. The inverse method for the logic of bunched implications. In LPAR, pages 466-480, 2004. Google Scholar
  8. Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. J. Symb. Log., 57(3):795-807, 1992. Google Scholar
  9. Didier Galmiche, Daniel Méry, and David J. Pym. The semantics of BI and resource tableaux. Mathematical Structures in Computer Science, 15(6):1033-1088, 2005. URL: http://dx.doi.org/10.1017/S0960129505004858.
  10. Steve Giambrone. TW_+ AND RW_+ ARE DECIDABLE. Journal of Philosophical Logic, 14(3):235-254, 1985. Google Scholar
  11. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  12. Rajeev Goré, Linda Postniece, and Alwen Tiu. Cut-elimination and proof search for bi-intuitionistic tense logic. CoRR, abs/1006.4793, 2010. Google Scholar
  13. Haskell B. Curry. A Theory of Formal Deductibility. University of Notre Dame, 1950. Google Scholar
  14. Norihiro Kamide. Temporal BI: Proof system, semantics and translations. Theor. Comput. Sci., 492:40-69, 2013. Google Scholar
  15. Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119-135, 1994. Google Scholar
  16. Stephen C. Kleene. Introduction to META-MATHEMATICS. North-Holland Publishing Co., 1952. Google Scholar
  17. Sonia Marin and Lutz Straßburger. Label-free Modular Systems for Classical and Intuitionistic Modal Logics. In Advances in Modal Logic, pages 387-406, 2014. Google Scholar
  18. Robert K. Meyer and Michael A. McRobbie. Multisets and relevant implication I. Australasian Journal of Philosophy, 60(3):107-139, 1982. Google Scholar
  19. Robert K. Meyer and Michael A. McRobbie. Multisets and relevant implication II. Australasian Journal of Philosophy, 60(3):265-281, 1982. Google Scholar
  20. Michael Moortgat. Categorial type logics. HANDBOOK OF LOGIC AND LANGUAGE, pages 93-177, 1997. Google Scholar
  21. Peter W. O'Hearn. On bunched typing. Journal of Functional Programming, 13(4):747-796, 2003. Google Scholar
  22. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. Google Scholar
  23. Dag Prawitz. Natural Deduction - A Proof-Theoretical Study. Almquist and Wiksell, 1965. Google Scholar
  24. David J. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Kluwer Academic Publishers, 2002. Google Scholar
  25. Anne S. Troelstra and Helmut Schwichtenberg. Basic proof theory (2nd ed.). Cambridge University Press, 2000. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact