Proof theory for indexed nested sequents

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 deduc-tive 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.

Domaines: Logique en informatique [cs.LO]

Sonia Marin, Lutz Strassburger. Proof theory for indexed nested sequents. TABLEAUX 2017 - Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2017, Brasilia, Brazil. pp.81-97. ⟨hal-01635935⟩