Skip to Main content Skip to Navigation
Conference papers

Cut Elimination in Nested Sequents for Intuitionistic Modal Logics

Lutz Strassburger 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
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Monday, January 7, 2013 - 1:00:48 PM
Last modification on : Thursday, January 20, 2022 - 5:30:45 PM
Long-term archiving on: : Monday, April 8, 2013 - 11:30:25 AM


Files produced by the author(s)




Lutz Strassburger. 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⟩



Record views


Files downloads