Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/trunk/src/eXene/demos/tactic-tree/HOW-TO-DEMO
ViewVC logotype

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

Parent Directory Parent Directory | Revision Log 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