Skip to Main content Skip to Navigation
New interface
Conference papers

Proof theory for indexed nested sequents

Sonia Marin 1 Lutz Strassburger 1 
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-01635935
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Wednesday, November 15, 2017 - 10:29:55 PM
Last modification on : Wednesday, February 2, 2022 - 3:55:21 PM
Long-term archiving on: : Friday, February 16, 2018 - 3:43:38 PM

File

Tableaux17.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01635935, version 1

Citation

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⟩

Share

Metrics

Record views

102

Files downloads

144