by Dirk Pattinson and Lutz Schröder
Abstract:
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.
Reference:
Dirk Pattinson and Lutz Schröder: Generic Modal Cut Elimination Applied to Conditional Logics, In Martin Giese, Arild Waaler, eds.: Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009), Lecture Notes in Computer Science, vol. 5607, pp. 280–294, Springer, 2009. [preprint]
Bibtex Entry:
@InProceedings{PattinsonSchroder09a,
author = {Dirk Pattinson and Lutz Schr{\"o}der},
title = {Generic Modal Cut Elimination Applied to Conditional Logics},
year = {2009},
editor = {Martin Giese and Arild Waaler},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5607},
pages = {280-294},
keywords = {Cut elimination modal logic conditional logic coalgebra},
comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/GenericCut.pdf"> [preprint] </a>},
abstract = {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.
},
}