TY - GEN
T1 - Generic modal cut elimination applied to conditional logics
AU - Pattinson, Dirk
AU - Schröder, Lutz
PY - 2009
Y1 - 2009
N2 - We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal modal logic. We give extensive example instantiations of our framework to various conditional logics. For these, we obtain fully internalised calculi which are substantially simpler than those known in the literature, along with leaner proofs of cut elimination and complexity. In one case, conditional logic with modus ponens and conditional excluded middle, cut elimination and complexity are explicitly stated as open in the literature.
AB - We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal modal logic. We give extensive example instantiations of our framework to various conditional logics. For these, we obtain fully internalised calculi which are substantially simpler than those known in the literature, along with leaner proofs of cut elimination and complexity. In one case, conditional logic with modus ponens and conditional excluded middle, cut elimination and complexity are explicitly stated as open in the literature.
UR - http://www.scopus.com/inward/record.url?scp=77956337758&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-02716-1_21
DO - 10.1007/978-3-642-02716-1_21
M3 - Conference contribution
SN - 3642027156
SN - 9783642027154
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 280
EP - 294
BT - Automated Reasoning with Analytic Tableaux and Related Methods - 18th International Conference, TABLEAUX 2009, Proceedings
T2 - 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009
Y2 - 6 July 2009 through 10 July 2009
ER -