Skip to Main content Skip to Navigation
Conference papers

Proof theory for indexed nested sequents

Sonia Marin 1 Lutz Straßburger 1
1 PARSIFAL - Proof search and reasoning with logic specifications
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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 metadatas

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-01635935
Contributor : Lutz Straßburger <>
Submitted on : Wednesday, November 15, 2017 - 10:29:55 PM
Last modification on : Thursday, March 5, 2020 - 6:35:41 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

Collections

Citation

Sonia Marin, Lutz Straßburger. 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

184

Files downloads

211