Skip to Main content Skip to Navigation
Journal articles

On Nested Sequents for Constructive Modal Logics

Ryuta Arisaka 1 Anupam Das 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
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 <>
Submitted on : Wednesday, December 2, 2015 - 1:43:09 PM
Last modification on : Friday, April 30, 2021 - 10:02:40 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

Collections

Citation

Ryuta Arisaka, Anupam Das, Lutz Straßburger. 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

416

Files downloads

529