Document Open Access Logo

Modular Focused Proof Systems for Intuitionistic Modal Logics

Authors Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.16.pdf
  • Filesize: 0.59 MB
  • 18 pages

Document Identifiers

Author Details

Kaustuv Chaudhuri
Sonia Marin
Lutz Straßburger

Cite AsGet BibTex

Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Modular Focused Proof Systems for Intuitionistic Modal Logics. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.16

Abstract

Focusing is a general technique for syntactically compartmentalizing the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing is usually specified as a restriction of the sequent calculus, the technique has not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some of the logics of the modal cube. We have recently extended the focusing technique to classical nested sequents, a generalization of ordinary sequents. In this work we further extend focusing to intuitionistic nested sequents, which can capture all the logics of the intuitionistic S5 cube in a modular fashion. We present an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.
Keywords
  • intuitionistic modal logic
  • focusing
  • proof search
  • cut elimination
  • nested sequents

Metrics

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

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. of Logic and Computation, 2(3):297-347, 1992. URL: http://dx.doi.org/10.1093/logcom/2.3.297.
  2. Arnon Avron. The method of hypersequents in the proof theory of propositional non-classical logics. In Logic: from foundations to applications: European logic colloquium, pages 1-32. Clarendon Press, 1996. Google Scholar
  3. Taus Brock-Nannestad and Carsten Schürmann. Focused natural deduction. In LPAR 17, volume 6397 of LNCS, pages 157-171, Yogyakarta, Indonesia, 2010. Springer. URL: http://dx.doi.org/10.1007/978-3-642-16242-8_12.
  4. Kai Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48(6):551-577, 2009. Google Scholar
  5. Kai Brünnler and Lutz Straßburger. Modular sequent systems for modal logic. In Martin Giese and Arild Waaler, editors, Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX'09, volume 5607 of LNCS, pages 152-166. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02716-1_12.
  6. Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger. The focused calculus of structures. In CSL, (LIPIcs), pages 159-173. Schloss Dagstuhl-LZI, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2011.159.
  7. Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Focused and synthetic nested sequents. In Bart Jacobs and Christof Löding, editors, FoSSaCS, April 2016. To appear. Google Scholar
  8. Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. J. of Autom. Reasoning, 40(2-3):133-177, 2008. URL: http://dx.doi.org/10.1007/s10817-007-9091-0.
  9. François Lamarche. On the algebra of structural contexts. Technical report, INRIA, 2006. Available at https://hal.inria.fr/inria-00099461; to appear in MSCS.
  10. Olivier Laurent. A proof of the focalization property in linear logic. Unpublished note, 2004. Google Scholar
  11. Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, 2009. URL: http://dx.doi.org/10.1016/j.tcs.2009.07.041.
  12. Sonia Marin and Lutz Straßburger. Label-free modular systems for classical and intuitionistic modal logics. In Advances in Modal Logic (AIML-10), 2014. Google Scholar
  13. Sean McLaughlin and Frank Pfenning. Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic. In 15th LPAR, volume 5330 of LNCS, pages 174-181, 2008. Google Scholar
  14. 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. Google Scholar
  15. Sara Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34(5-6):507-544, 2005. URL: http://dx.doi.org/10.1007/s10992-005-2267-3.
  16. Gordon D. Plotkin and Colin Stirling. A framework for intuitionistic modal logics. In 1st Conference on Theoretical Aspects of Reasoning about Knowledge, pages 399-406. Morgan Kaufmann, 1986. Google Scholar
  17. Jason Reed and Frank Pfenning. Focus-preserving embeddings of substructural logics in intuitionistic logic. Draft manuscript, January 2010. Google Scholar
  18. Gisèle Fischer Servi. Axiomatizations for some intuitionistic modal logics. Rendiconti del Seminario Matematico dell' Università Politecnica di Torino, 42(3):179-194, 1984. Google Scholar
  19. Robert J. Simmons. Structural focalization. ACM Trans. Comput. Log., 15(3):21:1-21:33, 2014. URL: http://dx.doi.org/10.1145/2629678.
  20. Alex Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh, 1994. Google Scholar
  21. Lutz Straßburger. Cut elimination in nested sequents for intuitionistic modal logics. In 16th International Conference on Foundations of Software Science and Computation Structures (FOSSACS), volume 7794 of LNCS, pages 209-224. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-37075-5_14.
  22. Noam Zeilberger. Focusing and higher-order abstract syntax. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 359-369. ACM, 2008. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact