Cut Elimination in Nested Sequents for Intuitionistic Modal Logics

Lutz Straßburger 1, 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : We present cut-free deductive systems without labels for the intuitionistic variants of the modal logics obtained by extending IK with a subset of the axioms d, t, b, 4, and 5. For this, we use the formalism of nested sequents, which allows us to give a uniform cut elimination argument for all 15 logic in the intuitionistic S5 cube.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/hal-00770678
Contributor : Lutz Straßburger <>
Submitted on : Monday, January 7, 2013 - 1:00:48 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Document(s) archivé(s) le : Monday, April 8, 2013 - 11:30:25 AM

Files

nested-int-mod-fossacs13-HAL.p...
Files produced by the author(s)

Identifiers

Collections

Citation

Lutz Straßburger. Cut Elimination in Nested Sequents for Intuitionistic Modal Logics. FoSSaCS 2013, Mar 2013, Rome, Italy. pp.209-224, ⟨10.1007/978-3-642-37075-5_14⟩. ⟨hal-00770678⟩

Share

Metrics

Record views

248

Files downloads

232