Cut Elimination in Nested Sequents for Intuitionistic Modal Logics

Lutz Strassburger (1, 2)

1 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
2 PARSIFAL - Proof search and reasoning with logic specifications

We present cut-free deductive systems without labels for the intuitionistic variants of the modal logics obtained by extending IK with a subset of the axioms d, t, b, 4, and 5. For this, we use the formalism of nested sequents, which allows us to give a uniform cut elimination argument for all 15 logic in the intuitionistic S5 cube.

Domaines: Logique en informatique [cs.LO]

Lutz Strassburger. Cut Elimination in Nested Sequents for Intuitionistic Modal Logics. FoSSaCS 2013, Mar 2013, Rome, Italy. pp.209-224, ⟨10.1007/978-3-642-37075-5_14⟩. ⟨hal-00770678⟩