Maehara-style modal nested calculi

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 :
Article dans une revue
Archive for Mathematical Logic, Springer Verlag, 2018, 〈10.1007/s00153-018-0636-1〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01942240
Contributeur : Lutz Straßburger <>
Soumis le : lundi 3 décembre 2018 - 11:32:02
Dernière modification le : mercredi 5 décembre 2018 - 01:14:25

Fichier

10.1007%2Fs00153-018-0636-1.pd...
Publication financée par une institution

Identifiants

Citation

Roman Kuznets, Lutz Straßburger. Maehara-style modal nested calculi. Archive for Mathematical Logic, Springer Verlag, 2018, 〈10.1007/s00153-018-0636-1〉. 〈hal-01942240〉

Partager

Métriques

Consultations de la notice

18

Téléchargements de fichiers

10