Cut Elimination in Nested Sequents for Intuitionistic Modal Logics

Lutz Straßburger 1, 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We present cut-free deductive systems without labels for the intuitionistic variants of the modal logics obtained by extending IK with a subset of the axioms d, t, b, 4, and 5. For this, we use the formalism of nested sequents, which allows us to give a uniform cut elimination argument for all 15 logic in the intuitionistic S5 cube.
Type de document :
Communication dans un congrès
Frank Pfenning. FoSSaCS 2013, Mar 2013, Rome, Italy. Springer, 7794, pp.209-224, 2013, LNCS. 〈10.1007/978-3-642-37075-5_14〉
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-00770678
Contributeur : Lutz Straßburger <>
Soumis le : lundi 7 janvier 2013 - 13:00:48
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : lundi 8 avril 2013 - 11:30:25

Fichiers

nested-int-mod-fossacs13-HAL.p...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Lutz Straßburger. Cut Elimination in Nested Sequents for Intuitionistic Modal Logics. Frank Pfenning. FoSSaCS 2013, Mar 2013, Rome, Italy. Springer, 7794, pp.209-224, 2013, LNCS. 〈10.1007/978-3-642-37075-5_14〉. 〈hal-00770678〉

Partager

Métriques

Consultations de la notice

198

Téléchargements de fichiers

183