@inproceedings{65378330384746359ee9157faaec2f49,
title = "Modular focused proof systems for intuitionistic modal logics",
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 = "Cut elimination, Focusing, Intuitionistic modal logic, Nested sequents, Proof search",
author = "Kaustuv Chaudhuri and Sonia Marin and Lutz Stra{\ss}burger",
note = "Publisher Copyright: {\textcopyright} 2016 Kaustuv Chaudhuri, Sonia Marin, and Lutz Stra{\ss}burger.; 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 ; Conference date: 22-06-2016 Through 26-06-2016",
year = "2016",
month = jun,
day = "1",
doi = "10.4230/LIPIcs.FSCD.2016.16",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Delia Kesner and Brigitte Pientka",
booktitle = "1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016",
}