We give an example of a simple Watson proof to flesh out the abstract discussion above. Watson is implemented in SML, and its commands are ML function evaluations. Commands end with semicolons; more than one command may be put on a line. A command with no apparent arguments needs the null argument () of ML. Most parameters passed to commands are strings, and so are enclosed in double quotes ". Comments may be enclosed in decorated parentheses (* *) (in what follows we take the liberty of commenting not only code but also the term displays, in a way which would not happen in real Watson output). The prover normally displays additional prompts, which are suppressed here for compactness of presentation. The prompt at which an ML command to the prover is entered is -.
(* some declarations needed for setup *)
- declareinfix "+";
- axiom "COMM" "?x+?y" "?y+?x";
- axiom "ASSOC" "(?x+?y)+?z" "?x+?y+?z";
(* We begin the proof of a simple theorem. "s" is an
abbreviation for "start", the full name of the command
which starts a proof. *)
- s "?x+?y+?z";
{?x + ?y + ?z} (* the resulting display *)
?x + ?y + ?z
(* We demonstrate navigation commands. *)
- left();
{?x} + ?y + ?z (* the resulting display *)
?x
- up(); (* returns to previous
position; display omitted *)
(* We start the proof. *)
- ri "COMM"; ex(); (* introduce a rewrite rule
(ri abbreviates ruleintro);
invoke tactic interpreter *)
{COMM => ?x + ?y + ?z} (* display after ri *)
COMM => ?x + ?y + ?z
{(?y + ?z) + ?x} (* display after execution *)
(?y + ?z) + ?x
- left(); ri "COMM"; ex(); (* move to left subterm,
introduce rewrite rule,
invoke tactic interpreter *)
{?y + ?z} + ?x (* display after left *)
?y + ?z
{COMM => ?y + ?z} + ?x (* display after
COMM => ?y + ?z introducing rewrite *)
{?z + ?y} + ?x (* display after executing
?z + ?y tactic interpreter *)
- up(); ri "ASSOC"; ex(); (* move up, introduce rewrite
(associativity)
then use tactic interpreter *)
{(?z + ?y) + ?x} (* display after moving up *)
(?z + ?y) + ?x
{ASSOC => (?z + ?y) + ?x} (* display after
ASSOC => (?z + ?y) + ?x introducing rewrite rule *)
{?z + ?y + ?x} (* display after executing
?z + ?y + ?x tactic interpreter *)
- p "REVERSE"; (* prove new theorem REVERSE *)
REVERSE: (* resulting theorem display *)
?x + ?y + ?z =
?z + ?y + ?x
ASSOC , COMM , 0 (* dependencies on axioms *)
- s "?a+?b+?c+?d"; (* test new theorem *)
{?a + ?b + ?c + ?d} (* display *)
?a + ?b + ?c + ?d
- ri "REVERSE"; ex(); (* introduce rewrite rule
and use tactic interpreter *)
{REVERSE => ?a + ?b + ?c + ?d}
REVERSE => ?a + ?b + ?c + ?d
{(?c + ?d) + ?b + ?a} (* display of final result *)
(?c + ?d) + ?b + ?a
A particular feature to which we wish to call the attention of the reader is the two-step handling of rewrite rules (introduction of a reference to the rewrite rule to be applied into the term, followed by invocation of the ``tactic interpreter'' execute (abbreviated ex)), which might seem odd. The reason for this should become evident in the next subsubsection.