## Paper: A Neutral Approach to Proof and Refutation in MALL (at LICS 2008)

**Olivier Delande Dale A. Miller**

### Abstract

We propose a setting in which the search for a proof of B or a refutation of B (a proof of not B) can be carried out simultaneously. In contrast with the usual approach in automated deduction, we do not need to first commit to either proving B or to proving not B: instead we devise a neutral setting for attempting both a proof and a refutation. This setting is described as a two player game in which each player follows the same rules. A winning strategy translates to a proof of the formula and a winning counter-strategy translates to a refutation of the formula. The game is described for multiplicative and additive linear logic without atomic formulas. A game theoretic treatment of the multiplicative connectives is intricate and our approach to it involves two important ingredients. First, labeled graph structures are used to represent positions in a game and, second, the game playing must deal with the failure of a given player and with an appropriate resumption of play. This latter ingredient accounts for the fact that neither players might win (that is, neither B nor not B might be provable).

### BibTeX

@InProceedings{DelandeMiller-ANeutralApproachtoP, author = {Olivier Delande and Dale A. Miller}, title = {A Neutral Approach to Proof and Refutation in MALL}, booktitle = {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)}, year = {2008}, month = {June}, pages = {498--508}, location = {Pittsburgh, PA, USA}, publisher = {IEEE Computer Society Press} }