Modular Focused Proof Systems for Intuitionistic Modal Logics

Kaustuv Chaudhuri 1 Sonia Marin 1 Lutz Straßburger 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
FSCD 2016 - 1st International Conference on Formal Structures for Computation and Deduction, Jun 2016, Porto, Portugal. 〈10.4230/LIPIcs.FSCD.2016.16〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01417603
Contributeur : Lutz Straßburger <>
Soumis le : jeudi 15 décembre 2016 - 17:15:06
Dernière modification le : mercredi 25 avril 2018 - 10:45:27

Identifiants

Collections

Citation

Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger. Modular Focused Proof Systems for Intuitionistic Modal Logics. FSCD 2016 - 1st International Conference on Formal Structures for Computation and Deduction, Jun 2016, Porto, Portugal. 〈10.4230/LIPIcs.FSCD.2016.16〉. 〈hal-01417603〉

Partager

Métriques

Consultations de la notice

154