Skip to Main content Skip to Navigation
Reports

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

Sonia Marin 1 Lutz Straßburger 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 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.
Document type :
Reports
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/hal-01515797
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Friday, April 28, 2017 - 10:54:24 AM
Last modification on : Wednesday, November 3, 2021 - 6:31:33 AM
Long-term archiving on: : Saturday, July 29, 2017 - 1:11:34 PM

File

RR-9061.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01515797, version 1

Citation

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

Share

Metrics

Record views

411

Files downloads

168