On nested sequents for constructive modal logics

DOI10.2168/LMCS-11(3:7)2015MaRDI QIDQ3196338zbMATH OpenFDO

Authors Ryuta Arisaka, Anupam Das, Lutz Straßburger

Publication date 29 October 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1505.06896

zbMATH Keywords

intuitionistic logicmodal logiccut-eliminationnested sequents

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

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.

Recommendations

• Cut elimination in nested sequents for intuitionistic modal logics
• Modular sequent systems for modal logic
• Proof theory for indexed nested sequents
• Label-free modular systems for classical and intuitionistic modal logics
• Constructive modal logics. I

Cited in

(30)

• Proof theory for indexed nested sequents
• Dual and axiomatic systems for constructive S4, a formally verified equivalence
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence
• Maehara-style modal nested calculi
• Nested sequents for intuitionistic logics
• Nested sequent calculi for normal conditional logics
• scientific article; zbMATH DE number 5917724 (Why is no real title available?)
• The Došen square under construction: a tale of four modalities
• Grafting hypersequents onto nested sequents
• Linear Nested Sequents, 2-Sequents and Hypersequents
• Nested sequents for intuitionistic modal logics via structural refinement
• Terminating calculi and countermodels for constructive modal logics
• Combining monotone and normal modal logic in nested sequents -- with countermodels
• Wijesekera-style constructive modal logics
• Modular sequent systems for modal logic
• Prefixed tableaus and nested sequents
• Cut-free Gentzen calculus for multimodal CK
• Intuitionistic non-normal modal logics: a general framework
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
• scientific article; zbMATH DE number 3841820 (Why is no real title available?)
• Constructive modal logics. I
• Nested sequents for provability logic GLP: FIG. 1.
• A modal logic for discretely descending chains of sets
• The principle of reflection via nested sequents
• From 2-sequents and linear nested sequents to natural deduction for normal modal logics
• Embedding constructive K into intuitionistic K
• Realization theorems for justification logics: full modularity
• On intuitionistic diamonds (and lack thereof)
• Cut elimination in nested sequents for intuitionistic modal logics
• scientific article; zbMATH DE number 6302922 (Why is no real title available?)

This page was built for publication: On nested sequents for constructive modal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196338)