Maehara-style Modal Nested Calculi

Lutz Straßburger 1, 2 Roman Kuznets 3
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We develop multi-conclusion nested sequent calculi for the fifteen logics of the intuitionistic modal cube between IK and IS5. The proof of cut-free completeness for all logics is provided both syntactically via a Maehara-style translation and semantically by constructing an infinite birelational countermodel from a failed proof search. Interestingly, the Maehara-style translation for proving soundness syntactically fails due to the hierarchical structure of nested sequents. Consequently, we only provide the semantic proof of soundness. The countermodel construction used to prove completeness required a completely novel approach to deal with two independent sources of non-termination in the proof search present in the case of transitive and Euclidean logics.
Type de document :
Rapport
[Research Report] RR-9123, Inria Saclay. 2017
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01644750
Contributeur : Lutz Straßburger <>
Soumis le : mercredi 22 novembre 2017 - 22:58:33
Dernière modification le : jeudi 10 mai 2018 - 02:06:59

Fichier

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

Identifiants

  • HAL Id : hal-01644750, version 1

Citation

Lutz Straßburger, Roman Kuznets. Maehara-style Modal Nested Calculi. [Research Report] RR-9123, Inria Saclay. 2017. 〈hal-01644750〉

Partager

Métriques

Consultations de la notice

201

Téléchargements de fichiers

49