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.