Davide Catta
LIRMM, Montpellier
Date(s) : 13/01/2022 iCal
10 h 30 min - 12 h 00 min
Les logiques modales constructives sont obtenues en étendant la logique propositionnelle intuitionniste avec certains axiomes modaux.
De nombreux systèmes de preuve sont connus pour ces logiques, cependant la seule sémantique dénotationnelle disponible est définie au moyen d’une construction abstraite, basée sur le quotient de leurs termes lambda. Dans cet exposé, nous présentons une sémantique dénotationnelle concrète pour la version constructive de la logique modale K (appelée CK). Notre sémantique est une sémantique des jeux. Nous présentons des stratégies gagnantes qui correspondent aux preuves de CK, nous montrons que nos stratégies gagnantes peuvent être composées, et que —de plus— notre sémantique est pleinement adéquate : chaque stratégie gagnante modale est l’interprétation d’une preuve de CK.
Cet exposé est basé sur : Matteo Acclavio, Davide Catta & Lutz Straßburger: Game Semantics for Constructive Modal Logic, TABLEAUX 2021, 428-445
Catégories