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

cut-eliminationintuitionistic logicmodal logicnested sequents

Mathematics Subject Classification ID

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

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

(35)

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

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)