A neutral approach to proofs and refutation in the setting of proof search
Ecole Polytechnique & INRIA Futurs.
I shall present preliminary results about an ongoing joint work with Dale Miller in which we attempt to describe a neutral approach to proof and refutation in the setting of proof search. We shall start with a discussion about Prolog and Horn Clauses that will lead us to the definition of neutral expressions. We use games based on neutral expressions in order to specify, in a neutral fashion, what it means to prove or refute by relating proofs/refutations and winning strategies in our games. Our study will deal with the richer Linear Logic rather than simply Horn Clauses.
We then present some examples of games based on neutral expressions and discuss some peculiar properties of neutral expressions and extensions we plan to study in the future.