2026-07-17T11:53:55Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5994 2024-03-06T10:37:25Z ddc:004 open_access

Modular Focused Proof Systems for Intuitionistic Modal Logics Chaudhuri, Kaustuv Marin, Sonia Straßburger, Lutz intuitionistic modal logic focusing proof search cut elimination nested sequents 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kaustuv Chaudhuri and Sonia Marin and Lutz Straßburger 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.16 urn:nbn:de:0030-drops-59947 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.16 eng https://creativecommons.org/licenses/by/3.0/legalcode