TY - GEN
T1 - Modular sequent systems for modal logic
AU - Brünnler, Kai
AU - Straßburger, Lutz
PY - 2009/1/1
Y1 - 2009/1/1
N2 - We see cut-free sequent systems for the basic normal modal logics formed by any combination the axioms d, t, b, 4, 5. These systems are modular in the sense that each axiom has a corresponding rule and each combination of these rules is complete for the corresponding frame conditions. The systems are based on nested sequents, a natural generalisation of hypersequents. Nested sequents stay inside the modal language, as opposed to both the display calculus and labelled sequents. The completeness proof is via syntactic cut elimination.
AB - We see cut-free sequent systems for the basic normal modal logics formed by any combination the axioms d, t, b, 4, 5. These systems are modular in the sense that each axiom has a corresponding rule and each combination of these rules is complete for the corresponding frame conditions. The systems are based on nested sequents, a natural generalisation of hypersequents. Nested sequents stay inside the modal language, as opposed to both the display calculus and labelled sequents. The completeness proof is via syntactic cut elimination.
UR - https://www.scopus.com/pages/publications/77956310890
U2 - 10.1007/978-3-642-02716-1_12
DO - 10.1007/978-3-642-02716-1_12
M3 - Conference contribution
AN - SCOPUS:77956310890
SN - 3642027156
SN - 9783642027154
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 152
EP - 166
BT - Automated Reasoning with Analytic Tableaux and Related Methods - 18th International Conference, TABLEAUX 2009, Proceedings
PB - Springer Verlag
T2 - 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009
Y2 - 6 July 2009 through 10 July 2009
ER -