Skip to Main content Skip to Navigation
Journal articles

On Nested Sequents for Constructive Modal Logics

Ryuta Arisaka 1 Anupam Das 1 Lutz Strassburger 1 
1 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 deductive systems for various modal logics that can be obtained from the constructive variant of the normal modal logic CK by adding combinations of the axioms d, t, b, 4, and 5. This includes the constructive variants of the standard modal logics K4, S4, and S5. We use for our presentation the formalism of nested sequents and give a syntactic proof of cut elimination.
Document type :
Journal articles
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Wednesday, December 2, 2015 - 1:43:09 PM
Last modification on : Tuesday, January 25, 2022 - 11:44:06 AM
Long-term archiving on: : Saturday, April 29, 2017 - 12:18:22 AM


Publisher files allowed on an open archive


Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License



Ryuta Arisaka, Anupam Das, Lutz Strassburger. On Nested Sequents for Constructive Modal Logics. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2015, 11 (3), pp.1-33. ⟨10.2168/LMCS-11(3:7)2015⟩. ⟨hal-01093143v2⟩



Record views


Files downloads