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

Authors: 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}
  }