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
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 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 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 : Wednesday, March 27, 2019 - 4:41:29 PM
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

296

Files downloads

103