Generic Modal Cut Elimination Applied to Conditional Logics

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...

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2011-03, Vol.7, Issue 1
Main Authors: Pattinson, Dirk, Schröder, Lutz
Format: Article
Language:English
Subjects:
computer science - logic in computer science
f.4.1, i.2.3
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 were explicitly stated as open in the literature.
ISSN:1860-5974
1860-5974
DOI:10.2168/LMCS-7(1:4)2011