Niveau: Supérieur
A neutral approach to proof and refutation in MALL Olivier Delande and Dale Miller INRIA Saclay - Ile-de France and LIX/ Ecole Polytechnique Route de Saclay, 91128 PALAISEAU Cedex FRANCE delande at lix.polytechnique.fr, dale.miller at inria.fr Abstract We propose a setting in which the search for a proof of B or a refutation of B (a proof of ¬B) can be carried out simultaneously: this is in contrast to the usual approach in automated deduction where we need to commit to proving either B or ¬B. Our neutral approach to proof and refuta- tion 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 trans- lates 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 player might win (that is, neither B nor ¬B might be provable). 1. Introduction Consider the behavior of an idealized Prolog interpreter given a noetherian logic program ∆ and query G.
- troduction rules
- guarded neutral
- injected into
- linear logic
- purely additive
- neutral graph
- without atoms
- expressions such