Skip to Main content Skip to Navigation

Symmetric dialogue games in the proof theory of linear logic

Olivier Delande 
Abstract : This thesis develops an original approach to the interactive interpretation of the proof theory of linear logic. In contrast with the player/opponent dichotomy commonly associated with game semantics for logic, we propose a model in which the two players have symmetric roles. More precisely, we shift from a situation in which a player aims at proving a goal while the other one aims at refuting it to a situation in which the players aim at proving opposite goals. In the tradition of computation-as-proof-search, each step of the interaction is seen as a step in two orthogonal sequent calculus proof searches. To some extent, this work contributes to formalising the connections between proof search and proof normalisation. We first present a simple symmetric game for the additive fragment of linear logic, as a first introduction to dual proof search. We then introduce a much more involved symmetric game accounting for the multiplicative and additive fragment of linear logic. In order to get a full completeness result, we then develop a third, highly concurrent, symmetric game. Finally, we investigate a few extensions of our model.
Document type :
Complete list of metadata
Contributor : Ecole Polytechnique Connect in order to contact the contributor
Submitted on : Wednesday, June 30, 2010 - 8:00:00 AM
Last modification on : Wednesday, June 30, 2010 - 8:00:00 AM
Long-term archiving on: : Tuesday, October 23, 2012 - 9:45:18 AM


  • HAL Id : pastel-00006196, version 1



Olivier Delande. Symmetric dialogue games in the proof theory of linear logic. Computer Science [cs]. Ecole Polytechnique X, 2009. English. ⟨pastel-00006196⟩



Record views


Files downloads