Publikation
Cut Elimination in Coalgebraic Logics
Dirk Pattinson; Lutz Schröder
In: Information and Computation (Inform. Comput.), Vol. 208, Pages 1447-1468, Elsevier, Amsterdam, 12/2010.
Zusammenfassung
We give two generic proofs for cut elimination in propositional modal logics, interpreted over coalgebras. We first investigate semantic coherence conditions between the axiomatisation of a particular logic and its coalgebraic semantics that guarantee that the cut-rule is admissible in the ensuing sequent calculus. We then independently isolate a purely syntactic property of the set of modal rules that guarantees cut elimination. Apart from the fact that cut elimination holds, our main result is that the syntactic and semantic assumptions are equivalent in case the logic is amenable to coalgebraic semantics. As applications we present a new proof of the (already known) interpolation property for coalition logic and newly establish the interpolation property for the conditional logics CK and CK+ID.
Projekte
FormalSafe - Formale Entwicklung für Sichere Robotik,
GenMod - Generische Algorithmen und Komplexitätsschranken für Koalgebraische Modallogiken
GenMod - Generische Algorithmen und Komplexitätsschranken für Koalgebraische Modallogiken