The message BCKMsg: asking for a move.

We compute if backtracking is allowed for turn n and player p.

In[315]:=

(* Backtracking is allowed if it not the case that the implication is material and the logic i ... t;Intuitionistic"]], n>1, Implies[CutFree, p"Eloise"]] ;

This is the input message remembering to a player p he can drop out of the play and lose, or (if allowed) backtrack to any previous position.

In[316]:=

OrDropBck[p_, n_] := If[BCKAllowed[p, n], "\nType \"drop\" to d ... t; to backtrack to position n.", "\nType \"drop\" to drop out"] ;

If the formula is ∃x.A,the player p moving next must choose and defend some instance A[i] of ∃x.A.

In[317]:=

BCKMsg[{Ex[x_, A_], s_}, n_, p_] := CompoundExpression[Print[PlayerLogo[p], " mus ... x,   " of the existential you want to defend. ", OrDropBck[p, n]] ] ;

If the formula is ∀x.A,the player p moving next must choose and attack some instance A[i] of ∀x.A.

In[318]:=

BCKMsg[{Un[x_, A_], s_}, n_, p_] := CompoundExpression[Print[PlayerLogo[p], " mus ... stance ", x, " of the universal you want to attack. ", OrDropBck[p, n]] ] ;

If the formula is A∨B,the player p moving next must choose and defend either A or B.

In[319]:=

BCKMsg[{Disj[A_, B_], s_}, n_, p_] := CompoundExpression[Print[PlayerLogo[p], " m ... ubformula, type R if you want to defend the right subformula. ", OrDropBck[p, n]] ] ;

If the formula is A∧B,the player p moving next must choose and attack either A or B.

In[320]:=

BCKMsg[{Conj[A_, B_], s_}, n_, p_] := CompoundExpression[Print[PlayerLogo[p], " m ... ubformula, type R if you want to attack the right subformula. ", OrDropBck[p, n]] ] ;

If the formula is A→B,the player p moving next must either choose and attack A or choose and defend B.

In[321]:=

BCKMsg[{HypImpl[A_, B_], s_}, n_, p_] := CompoundExpression[Print[PlayerLogo[p], " ... ubformula, type R if you want to defend the right subformula. ", OrDropBck[p, n]] ] ;

If the formula is A⇒B (in particular, if the implication is constructive) the player p moving next must attack A→B. There is no other choice (but backtracking or dropping out).

In[322]:=

BCKMsg[{Impl[A_, B_], s_}, n_, p_] := If[MaterialImplication, BCKMsg[{HypImpl[A, B], s ... quot;: type Box (or anything) to attack the only subformula. ", OrDropBck[p, n]] ]] ;

If the formula is ¬A, the player p moving next must attack A. There is no other choice (but backtracking or dropping out).

In[323]:=

BCKMsg[{Neg[A_], s_}, n_, p_] := CompoundExpression[Print[PlayerLogo[p], " must d ... ;: type Negation (or anything) to defend the only subformula. ", OrDropBck[p, n]] ] ;

If the formula is T, the player p moving next gives up or backtracks.

In[324]:=

BCKMsg[{TrueAtom, s_}, n_, p_] := CompoundExpression[Print[PlayerLogo[p], " has n ... [n - 1], ".\n", p, ": True has no subformulas. ", OrDropBck[p, n]] ] ;

If the formula is F, the player p moving next gives up or backtracks.  

In[325]:=

BCKMsg[{FalseAtom, s_}, n_, p_] := CompoundExpression[Print[PlayerLogo[p], " has ... n - 1], ".\n", p, ": False has no subformulas. ", OrDropBck[p, n]] ] ;

If the formula is atomic ≠T, F, the program first unfold abbreviations. Then it asks for the truth value of A. If A is true, the next player moves T, if A is false, the next player moves F.

In[326]:=

BCKMsg[{A_String, s_}, n_, p_] := If[AbbreviationQ[A], BCKMsg[{Unfold[A], s}, ... type Atom (or anything) to defend the atom ", A, ".", OrDropBck[p, n]] ]] ;

Created by Mathematica  (October 17, 2006)