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.
Type de document :
Rapport
[Research Report] RR-9061, Inria. 2017
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01515797
Contributeur : Lutz Straßburger <>
Soumis le : vendredi 28 avril 2017 - 10:54:24
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : samedi 29 juillet 2017 - 13:11:34

Fichier

RR-9061.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

274

Téléchargements de fichiers

94