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

https://hal.inria.fr/hal-01093143
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

File

1505.06896.pdf
Publisher files allowed on an open archive

Licence


Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

419

Files downloads

172