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.
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/hal-01515797
Contributor : Lutz Straßburger <>
Submitted on : Friday, April 28, 2017 - 10:54:24 AM
Last modification on : Thursday, March 5, 2020 - 6:34:27 PM
Document(s) archivé(s) le : 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

312

Files downloads

113