How to give a tactic tree demo.
Suppose that the tactic tree code is in directory EXENE-DIR.
Documentation can be found in EXENE-DIR/demos/tactic-tree/doc/doc.ps.
Here is how to get started with a demo:
% eXene
- System.Directory.cd "EXENE-DIR/demos/tactic-tree/src";
- use "load";
- System.Directory.cd "../examples/fol";
- use "load-fol";
This will leave you with two functions,
val create : string * string * (string * tactic) list -> ttree_state
val view : ttree_state * string * (string * tactic) list -> ttree_state
and some example formulas,
val p1 = "A' -> B' -> (A' & B')" : string
val p2 = "A' -> B' -> C' -> ((A' & B') & (B' & C'))" : string
val p3 = " (P' -> (Q' | R')) -> ((P' ->Q') | (P' ->R'))" : string
val p4 = "((A' | B') -> C') -> ((A' -> C') & (B' -> C'))" : string
To prove p4, enter
- val p = create(p4,"",[]) ;
this will pop up a tactic tree window (on display "", the current display, with
an empty list of auxiliary tactics).
Upon exiting the tactic tree window, p is bound to a tactic tree state.
This state can be revisited by
- view(p,"",[]) ;