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

SCM Repository

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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2 - (download) (annotate)
Sat Oct 4 23:33:09 1997 UTC (22 years, 10 months ago) by monnier
File size: 1104 byte(s)
Initial revision

	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,"",[]) ; 



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