Project topics and materials
Get Complete Project Material File(s) Now! »
Proof theory and computation
In the general context of the study of computation, approaches to proof theory traditionally fall into two categories. In the computation-as-proof-normalisation approach, proofs model programs in functional languages. The computational content of this model is seen in the correspondence between proof normalisation and program execution. In that setting, a formula is a type, and a proof is a term of that type. A formula is true iff its type is not empty. Implication corresponds to the “arrow” constructor for types and plays a fundamental role. Proofs of A → B are functions mapping proofs of A to proofs of B. Proof normalisation corresponds to β-reduction in λ-calculus.
In the computation-as-proof-search approach, the state of the computation is seen as a sequent, and the computation itself as the search for a cut-free proof of that sequent. This is the basis for logic programming [MNPS91]. In that tradition, the specific features of a proof system are used to model proof search strategies. For example, the bias assignment to the atoms in a focused proof system can force forward-chaining or back-chaining [LM07].
Games and logic
The connections between logic and games have a long and rich history, although they remained informal until the 1950s. It is known since Aristotle that a debate can be seen as a game. The twentieth century saw the development of game theory, and connections were then made to logic. From the point of view of game theorists in general, the kinds of games studied in logic are quite specific. They typically involve two players with distinct roles, are not concerned with probabilities, and usually have two outcomes: a win for a player or for the opponent.
In a typical game for logic, the two players, called the Player and the Opponent, or ´Elo¨ıse and Ab´elard, build a sequence of moves called a play. For each finite sequence of moves, the rules of the game specify which player shall be the one to extend the sequence with a move, and which moves are at her disposal for doing so. Plays may be infinite in general, but there may also be some finite sequences of moves that cannot be extended with additional moves. In either case, the rules of the game classify maximal plays into those won by ´E lo¨ıse and those won by Ab´elard. The plays are the uni-dimensional objects of the games. There are also bi-dimensional objects of interest called strategies. Strategies represent move policies that players may follow. A typical strategy is simply a set of plays that a player is prepared to follow. An important question about the game is whether a specific player can play according to some strategy which ensures her victory. If the answer is positive, then such strategies, called winning strategies, are formal witnesses to this fact. Similarly, proofs are witnesses to the truth of a formula. The games we are interested in tend to make this connection between games/formulae, provability/the existence of a winning strategy, proofs/winning strategies, and computation/dynamics of interaction. Dialogue games were formalised by Lorenzen [Lor61]. In those games, the Player tries to establish the truth of a formula while the Opponent tries to establish its falsehood. Informally, the Opponent plays the role of an examiner and the Player plays the role of an examinee. For example, if the formula is a conjunction, the Opponent chooses a conjunct and challenges the Player to prove it; if it is a disjunction, the Player chooses which disjunct to prove.
Computation as dual proof search
In the above example, the player who starts does not have a winning strategy.
Determining it requires to explore the arena much like a search space in proof search. This graph exploration progressively partitions the positions in two sets, starting from the terminal ones, depending on which player has a winning strategy for them. This process not only does this classification, but it also builds winning strategies. Since steps in the game (micro-moves and macromoves) correspond to steps in proofs (rules and phases), it is clear that the exploration of the arena builds derivations gradually. In this respect, this game is deeply rooted in the tradition of computation as proof search. An interesting aspect of this computation is that we always get a winning strategy in the end (hence a proof), but we do not know for which player until we finish. Hence, the computation can be seen as the simultaneous development of two dual derivations, one of which will eventually be closed to become a proof.
Table of contents :
Introduction
1 Preliminaries
1.1 First-order classical logic
1.2 Sequent calculus
1.3 Linear logic
1.4 Focalisation
1.5 Multifocalisation
1.6 Proof theory and computation
1.7 Games and logic
1.8 The neutral approach
2 Additive neutral games
2.1 An additive neutral game
2.1.1 Hintikka’s additive game for truth
2.1.2 A neutral presentation
2.1.3 Computation as dual proof search
2.1.4 Interaction as proof normalisation
2.2 Simple games for a fragment of MALL
3 A sequential neutral game for MALL
3.1 Unrestricted multiplicatives
3.1.1 Incompleteness
3.1.2 Concurrency and focusing
3.2 Proof system
3.3 Basic definitions
3.4 Neutral expressions
3.5 Neutral graphs
3.5.1 Interacting multiplicatives
3.5.2 A neutral presentation
3.6 Positions and moves
3.6.1 Positions
3.6.2 Micro-moves
3.6.3 Macro-moves
3.7 Examples
3.7.1 Indeterminacy
3.7.2 Atoms
3.8 Winning strategies and cut-free proofs
4 A concurrent neutral game for MALL
4.1 Introduction
4.1.1 Non-uniformity
4.1.2 Locality and concurrency
4.1.3 The [⊤] rule
4.1.4 Failure
4.2 Proof system
4.3 Neutral graphs
4.4 Subgraphs
4.5 Micro-moves
4.6 Macro-moves and positions
4.6.1 Definition
4.6.2 Macro-moves as phases
4.7 Strategies
4.8 Winning strategies and proofs
4.8.1 Strategy classes
4.8.2 Goal trees
5 Extensions
5.1 Explicit cuts
5.1.1 Infinite interactions
5.1.2 An alternate cut micro-move
5.1.3 Winning strategies and proofs
5.2 Exponentials
5.3 First-order quantification
5.4 Equality
5.5 Fixed points
6 Related and future work
7 Conclusion
