A Game Semantics for Proof Search: Preliminary Results

We describe an ongoing project in which we attempt to describe a neutral approach to proof and refutation. In particular, we present a language of neutral expressions which contains one element for each de Morgan pair of connectives in (linear) logic. Our goal is then to describe, in a neutral fashion, what it means to prove or refute. For this, we use games where moves are described as transitions between positions built with neutral expressions. In some settings, we can then relate winning a game with provability or with validity.