TY - GEN
T1 - Cut elimination in nested sequents for intuitionistic modal logics
AU - Straßburger, Lutz
PY - 2013/3/5
Y1 - 2013/3/5
N2 - We present cut-free deductive systems without labels for the intuitionistic variants of the modal logics obtained by extending IK with a subset of the axioms d, t, b, 4, and 5. For this, we use the formalism of nested sequents, which allows us to give a uniform cut elimination argument for all 15 logic in the intuitionistic S5 cube.
AB - We present cut-free deductive systems without labels for the intuitionistic variants of the modal logics obtained by extending IK with a subset of the axioms d, t, b, 4, and 5. For this, we use the formalism of nested sequents, which allows us to give a uniform cut elimination argument for all 15 logic in the intuitionistic S5 cube.
U2 - 10.1007/978-3-642-37075-5_14
DO - 10.1007/978-3-642-37075-5_14
M3 - Conference contribution
AN - SCOPUS:84874429388
SN - 9783642370748
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 209
EP - 224
BT - Foundations of Software Science and Computation Structures - 16th Int. Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proc.
T2 - 16th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013
Y2 - 16 March 2013 through 24 March 2013
ER -