Fully structured proof theory for intuitionistic modal logics

Sonia Marin (1) , Marianela Morales (2)

1 UCL - University College of London [London]
2 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion

We present a labelled sequent system and a nested sequent system for intuitionistic modal logics equipped with two relation symbols, one for the accessibility relation associated with the Kripke semantics for modal logics and one for the preorder relation associated with the Kripke semantics for intuitionistic logic. Both systems are in close correspondence with the bi-relational Kripke semantics for intuitionistic modal logic.

Mots clés: Proof theory; Intuitionistic modal logic; Labelled sequents; Nested sequents

Domaines: Informatique [cs]; Mathématiques [math]

Sonia Marin, Marianela Morales. Fully structured proof theory for intuitionistic modal logics. AiML 2020 - Advances in Modal Logic, Aug 2020, Helsinki, Finland. ⟨hal-03048959⟩