MFPS XX1 Preliminary Version

Niveau: Supérieur
MFPS XX1 Preliminary Version A game semantics for proof search: Preliminary results 1 Dale Miller and Alexis Saurin 2 INRIA-Futurs and Ecole Polytechnique Palaiseau, France Abstract 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. Key words: proof theory, game semantics, neutral approach to proof and refutation. 1 Introduction Connections between games and logic are rather old and numerous [13]. Dia- log games support the intuitive ideal that if one has a proof of a proposition, one can always win against an opponent attempting to attack that proposi- tion [6,16]. In the domain of linear logic, various categories of games have been designed to give an abstract meaning to proofs and to proof normaliza- tion [1,4,10,14]. We will be interested in linear logic here as well but from the computation-as-proof-search perspective [19].

• such proof


• prolog interpreter


• linear logic


• translate neutral


• proof theory


• order mall


• neutral expressions


• argument expression