Pattinson, Dirk and Schröder, Lutz - Generic Modal Cut Elimination Applied to Conditional Logics

lmcs:968 - Logical Methods in Computer Science, March 17, 2011, Volume 7, Issue 1
Generic Modal Cut Elimination Applied to Conditional Logics

Authors: Pattinson, Dirk and Schröder, Lutz

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.

DOI : 10.2168/LMCS-7(1:4)2011
Volume: Volume 7, Issue 1
Published on: March 17, 2011
Submitted on: June 24, 2010
Keywords: Computer Science - Logic in Computer Science,F.4.1, I.2.3


Consultation statistics

This page has been seen 197 times.
This article's PDF has been downloaded 233 times.