§4.2 How to use the program ``BCK''

Installing the program ``BCK''. You need Mathematica interpreter of Wolfram co. to install it. Select the title: ``A program implementing ...'', then press Shift+Enter and wait a few seconds.

Calling the program ``BCK''. The program is started by executing (i.e., by copying into a free location, then pressing Shift+Enter):

    BCK[Formula, Arg1, Arg2, ... ]

What ``BCK'' does. You can play several kind of backtracking games for a given formula, drawing each position in tree form. If you want Tarski plays (no backtracking), no cut-rule, and Material Implication, add as argument the string: Intuitionistic, CutFree, MaterialImplication. If you want irreversible backtracking, no cut-rule, and Material Implication, add as argument the string: LCM, CutFree, MaterialImplication. If you want reversible backtracking, no cut-rule, and Material Implication, add as argument the string: Classical, CutFree, MaterialImplication. If you want intuitionistic backtracking, and constructive implication (like in this section), add as argument the string: Intuitionistic, CutFree, Constructive Implication

Input form for formulas. Variables, terms, and atomic formulas are written between "...", for instance: "x", y", "x<y". Compound formulas are written using the operators: Conj[A,B], Disj[A,B], Impl[A,B], Neg[A], Un["x",A], Ex["x",A], denoting A∧B, A∨B, A⇒B, ¬A, ∀x.A, ∃x.A. For instance, ∀x.∃y.(x<y) becomes Un["x",Ex["y","x<y"]]. If F is in input form, you can recover the usual syntax for F executing Lin[F].

Extra arguments. An extra argument can be a strings: par1, par2, par3=n, ..., where par1, par2, par3, ... are parameters. BCK[.] and Tarski[.] are in fact the same program, the only differences between them are the default values. If a parameter is not assigned, it is taken with the default value if any, otherwise with the previous value.
Parameters. FontSize=... (say: 12,14,18, ..). TreeWidth=... (in pixels). LevelHeight=... (height in pixels of each level of the tree). View-Tree, TarskiPlay. The first one draws view-trees for both players, the second one only the current Tarski play. You can merge all parameters in one string, or divide them in more strings.

How the play runs. ``Tarski'' asks for a move the player who should move next. The player can answer: ``Left'',``Right'' for selecting the left- or right-hand side of a judgement t.A∧B, t.A∨B, t.A⇒B, or f.A∧B, f.A∨B, f.A⇒B; ``Negation'' to select the only subjudgement of a negation t.¬A or f.¬A; ``Atom'' for the only subformula of an atom t.a or f.a (t.T or f.T if a is true, and t.F or f.F is a is false) ; t (a closed term) for selecting the instance t.A[t/x] or f.A[t/x] of a quantification t.∀x.A, t.∃x.A, or f.∀x.A, f.∃x.A.
Eloise can also backtrack from node i to any previous node j<i, typing ``bck j''. In this case nodes i+1, .., j are temporarily retracted (they are drawn thinner). There is only one branch with thick edges, is the branch ending in the golden ball denoting the current position. If backtracking is irreversible (option LCM), Eloise can only backtrack to a node of this branch. If backtracking is reversible (option Classic), Eloise can backtrack to any node in the view-tree. If this node was retracted, now it is restored (its branch is drawn thick again). If backtracking is intuitionistic, Eloise can backtrack to any negative judgement in the view-tree, but only to the last positive judgement.
When the current node is an atomic formula A whose truth value is open, the program asks the player moving next for the truth value of A. The player should provide it in a consistent way.

Saved plays. An argument can be also a saved play, or an initial segment of it, in matrix form.Saved played in matrix form are available whenever a play ends. We can delete any number of lines at the end, save just an initial part of the play, then re-play just the initial part of the play.

Created by Mathematica  (November 11, 2006)