The program BCKInput returning the input.

We define a subprogram BCKInput taking the current position A, its sign s, and the move i from the player. BCKInput computes:
    1. the next formula Anext.
    2. its sign signnext.
    3. a label msg for the edge in the tree form of the game.
signnext is equal to s, unless we choose an assumption of A, in which case signnext = Dual of s.

If the formula is ∃x.A,the next formula is some instance A[i] of ∃x.A.

In[327]:=

BCKInput[{Ex[x_, A_], s_}, i_] := {Sub[A, x, i], s, StringJoin[x, "=", ToString[i]]} ;

If the formula is ∀x.A,the next formula is some instance A[i] of ∀x.A.

In[328]:=

BCKInput[{Un[x_, A_], s_}, i_] := {Sub[A, x, i], s, StringJoin[x, "=", ToString[i]]} ;

If the formula is A∨B,the the next formula is either A or B.

In[329]:=

BCKInput[{Disj[A_, B_], s_}, i_] := {If[i == "L", A, B], s, If[i"L", "Left", "Right"]} ;

If the formula is A∧B,the the next formula is either A or B.

In[330]:=

BCKInput[{Conj[A_, B_], s_}, i_] := {If[i == "L", A, B], s, If[i"L" , "Left", "Right"]} ;

If the formula is A⇒B,the the next formula A→B, if it is A→B, the next formula is either A or B, and in the first case the sign changes.

In[331]:=

BCKInput[{Impl[A_, B_], s_}, i_] := If[MaterialImplication, If[i == "L", {A, ... "L", Dual[s], s], If[i"L", "Left", "Right"]} ; *)

In[332]:=

BCKInput[{HypImpl[A_, B_], s_}, i_] := If[i == "L", {A, Dual[s], "Left"}, {B, s, "Right"}] ;

If the formula is ¬A, the next formula is A, and the sign changes.

In[333]:=

BCKInput[{Neg[A_], s_}, i_] := {A, Dual[s], "Negation"} ;

If the formula is T, there is no next formula.

In[334]:=

BCKInput[{TrueAtom, s_}, i_] := CompoundExpression[Print["From", TrueAtom, " you can only drop or backtrack"]] ;

If the formula is F, there is no next formula.

In[335]:=

BCKInput[{FalseAtom, s_}, i_] := CompoundExpression[Print["From", FalseAtom, " you can only drop or backtrack"]] ;

If the formula is atomic ≠T,F, if A is true, the next player moves T, otherwise he moves F.

In[336]:=

BCKInput[{A_String, s_}, i_] := If[AbbreviationQ[A], BCKInput[{Unfold[A], s}, i],  {If[TruthValue[A] == "true", TrueAtom, FalseAtom], s, "Atom"}] ;

Created by Mathematica  (October 17, 2006)