Seminari del Dipartimento

Logica e Informatica Teorica

Constructive modal logics are extensions of intuitionistic propositional logic with certain modal axioms. Many proof systems are known for these logics, but the only available denotational semantics is defined by means of an abstract construction, based on the quotient of their lambda terms.

The general aim of our work is to define a game semantics for constructive modal logics. In this talk, I will define the winning strategies for a formula and show the correspondence between winning strategies and proofs. I will show how winning strategies can be defined as the projection of specific paths in a graphical proof system defined for this purpose - combinatorial proofs.

(This talk is based on joint work with Matteo Acclavio and Lutz Straßburger)
org: PEDICINI Marco