Output details

Cut elimination in coalgebraic logics

<11>Cut elimination is a condicio-sine-qua-non in automated reasoning and induces decision procedures in the form of backwards proof search and is also the basis for interpolation. Usually, cut-elimination is established, in a tedious way, on a logic-by-logic basis. This paper instead presents a meta-theoretic result and isolates simple, local conditions on modal logics that have cut elimination as a consequence. As an application, we give new cut-free calculi and establish interpolation for a range of conditional logics. This paper has independently been verified using a theorem prover and so is an important step towards a generic treatment of logics.