Annotation of /sml/trunk/src/eXene/demos/tactic-tree/HOW-TO-DEMO

Parent Directory | Revision Log

---

Revision 2 - (view) (download)

1 :	monnier	2
2 :
3 :			How to give a tactic tree demo.
4 :
5 :			Suppose that the tactic tree code is in directory EXENE-DIR.
6 :
7 :			Documentation can be found in EXENE-DIR/demos/tactic-tree/doc/doc.ps.
8 :
9 :			Here is how to get started with a demo:
10 :
11 :			% eXene
12 :
13 :			- System.Directory.cd "EXENE-DIR/demos/tactic-tree/src";
14 :			- use "load";
15 :			- System.Directory.cd "../examples/fol";
16 :			- use "load-fol";
17 :
18 :			This will leave you with two functions,
19 :
20 :			val create : string * string * (string * tactic) list -> ttree_state
21 :			val view : ttree_state * string * (string * tactic) list -> ttree_state
22 :
23 :			and some example formulas,
24 :
25 :			val p1 = "A' -> B' -> (A' & B')" : string
26 :			val p2 = "A' -> B' -> C' -> ((A' & B') & (B' & C'))" : string
27 :			val p3 = " (P' -> (Q' | R')) -> ((P' ->Q') | (P' ->R'))" : string
28 :			val p4 = "((A' | B') -> C') -> ((A' -> C') & (B' -> C'))" : string
29 :
30 :			To prove p4, enter
31 :
32 :			- val p = create(p4,"",[]) ;
33 :
34 :			this will pop up a tactic tree window (on display "", the current display, with
35 :			an empty list of auxiliary tactics).
36 :
37 :			Upon exiting the tactic tree window, p is bound to a tactic tree state.
38 :			This state can be revisited by
39 :
40 :			- view(p,"",[]) ;
41 :
42 :

---

root@smlnj-gforge.cs.uchicago.edu	ViewVC Help
Powered by ViewVC 1.0.0