§0.2 A program implementing Game Semantic for Classical Logic and Constructive Implication.

Here is a program BCK  producing plays with backtracking, corresponding to a logic ranging from intuitionistic logic to LCM to classical logic. The logic can be cut-free or with cut-rule. The program BCK:
    1. draws the tree image of the current Tarski play, if the parameter DrawingTree is set to "TarskiPlay".
    2. Draws the memory (or "view") of each player who can backtrack, if the parameter DrawingTree is set to "View".  

BCK has three arguments: the judgment {A,s}, the turn n of the play, and the state {EView,AView,CurrentPlay} of the players and the play.EView is the first index (looking backwards) in the view of Eloise. AView is the first index  (looking backwards)  in the view of Abelard. CurrentPlay is the first index  (looking backwards) in the current Tarski play. CurrentPlay is in the view of both Eloise and Abelard, therefore CurrentPlay ≤ EView, AView ≤ n.
    1. A normal move adds one child, having index n+1 in the play, to the formula having index CurrentPlay. This child is added to the view of both players and to the current Tarski play, and becomes the last index in the three cases. The counter n is set to n+1.
    2. A backtrack move of Eloise replaces the current Tarski play by some previous one, by replacing the index CurrentPlay with some index i<CurrentPlay in the view of Eloise.   The view of Eloise and the counter n do not change. The view of Abelard becomes the view Abelard had from i.
    3. A backtrack move of Abelard replaces the current Tarski play by some previous one, by replacing the index CurrentPlay with some index i<CurrentPlay in the view of Abelard.   The view of Abelard and the counter n do not change. The view of Eloise becomes the view Eloise had from i.

If the new value of CurrentPlay is not in the previous current Tarski play, we say that Eloise restored some temporarely erased position. A backtracking position is not counted as a move of the play. We have a backtracking position if and only if CurrentPlay < n. In this case, we have CurrentPlay < EView if and only if Eloise did the last backtracking, and CurrentPlay < AView if and only if Abelard did the last backtracking.

The programs has two sets of parameters. The first set describes the formulas used in the backtracking plays.
    1. FormSign[n] is the sign of the position (i.e. judgment) number n.
    2. FormInd[n] is the formula of index n of the play.
    3. Branch[p,n] is the list of indexes of formulas available by 1-backtracking play for player p at step n.
    4. View[p,n,s] is the list of indexes of formulas of sign s in the view of player p at step n.
The current goal of player P at step n is the sequent View[p,n,neg]|-View[p,n,pos]. The formula of index CurrentPlay is the formula of View[p,n,neg]|-View[p,n,pos] that p want to prove (if positive) or disprove (if negative).

The second parameter set describes the trees used as comments. Let k="TarskiPlay", "Eloise", "Abelard" be the name of the tree describing: the current Tarski play, Eloise's view, Abelard's view.
    1. Tree[k,n] is the (unlabeled) tree of name k at step n.
    2. FormList[k,n] is the list of label assignments to vertices of Tree[k,n]. Each formula has sign, color, and (in a line below) the index of the formula, in black.
    3. MoveL[k,n] is the list of color and label assigments to edges of Tree[k,n+1]. Any move has the color of the player who did it, and is labelled with a coloured message describing the move.
    4. BranchCol[p,n] is the list of color assignments to the branch representing the current play inside Tree[p,n], for p=Abelard, Eloise. The color of the branch is the color of the player making the corresponding move, but heavier, to make it more evident. The color assignment BranchCol[p,n] is superposed to the color assignement MoveL[k,n].

Created by Mathematica  (October 17, 2006)