Skip to Main content Skip to Navigation
New interface
Conference papers

Game Semantics for Constructive Modal Logic

Matteo Acclavio 1 Davide Catta 2 Lutz Strassburger 3 
2 TEXTE - Exploration et exploitation de données textuelles
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
3 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : In this paper we provide the first game semantics for the constructive modal logic CK. We first define arenas encoding modal formulas, we then define winning innocent strategies for games on these arenas, and finally we characterize the winning strategies corresponding to proofs in the logic CK. To prove the full-completeness of our semantics, we provide a sequentialization procedure of winning strategies. We conclude the paper by proving their compositionality and showing how our results can be extend to the constructive modal logic CD.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03369819
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Thursday, October 7, 2021 - 3:48:29 PM
Last modification on : Friday, November 11, 2022 - 6:46:48 PM
Long-term archiving on: : Saturday, January 8, 2022 - 7:22:03 PM

File

Tableaux2021-Paper27.pdf
Files produced by the author(s)

Identifiers

Citation

Matteo Acclavio, Davide Catta, Lutz Strassburger. Game Semantics for Constructive Modal Logic. TABLEAUX 2021 - 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2021, Birmingham, United Kingdom. pp.428-445, ⟨10.1007/978-3-030-86059-2_25⟩. ⟨hal-03369819⟩

Share

Metrics

Record views

70

Files downloads

83