On the Proof Theory of Indexed Nested Sequents for Classical and Intuitionistic Modal Logics

Sonia Marin (1) , Lutz Strassburger (1)

1 PARSIFAL - Proof search and reasoning with logic specifications

Fitting's indexed nested sequents can be used to give deductive systems to modal logics which cannot be captured by pure nested sequents. In this paper we show how the standard cut-elimination procedure for nested sequents can be extended to indexed nested sequents, and we discuss how indexed nested sequents can be used for intuitionistic modal logics.

Mots clés: Indexed nested sequents; intuitionistic modal logics; cut elimination

Domaines: Logique en informatique [cs.LO]

Sonia Marin, Lutz Strassburger. On the Proof Theory of Indexed Nested Sequents for Classical and Intuitionistic Modal Logics. [Research Report] RR-9061, Inria. 2017. ⟨hal-01515797⟩