Paper Info
Title
A Neutral Approach to Proof and Refutation in MALL
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).
Year
DOI
Venue
2008
10.1109/LICS.2008.35
LICS
Keywords
Field
DocType
winning strategy translates,multiplicative connective,neutral setting,atomic formula,usual approach,neutral approach,player game,game playing,additive linear logic,game theoretic treatment,winning counter-strategy translates,calculus,labeling,game theory,additives,color,game semantics,games,linear logic,formal logic,computer science,propulsion,theorem proving,graph theory,switches,logic,automated deduction
Atomic formula,Two-player game,Discrete mathematics,Multiplicative function,Strategy,Computer science,Automated theorem proving,Game theory,Linear logic,Game semantics
Conference
ISSN
Citations 
PageRank 
1043-6871
8
0.66
References 
Authors
9
2
Name
Order
Citations
PageRank
Olivier Delande1161.57
Dale Miller22485232.26