The model of proof introduced in this subsection and exemplified in the previous subsubsection is effective in principle but tedious in practice. Watson provides a technique for executing many proof steps automatically, which may properly be discussed at this point. A program for executing proof steps automatically is called a ``tactic'' by a perhaps false analogy with usage in HOL and other provers of the LCF family. In those systems, a tactic is an ML program, an object of quite a different sort than a theorem. In Watson, a tactic is represented by the prover to itself as an equational theorem, but nonetheless may exhibit complex execution behavior. We describe here the way in which this effect is achieved.
The key feature of the language of Watson which makes the tactic language possible is the ability to represent the intention to apply a rewrite rule inside a term. This is done using the special infixes => and <=.
A term like (COMM => ?x + ?y) + ?z has precisely the same mathematical referent as the term (?x + ?y) + ?z. The presence of the embedded theorem COMM (a commutativity axiom) indicates the intention of applying the theorem COMM as a rewrite rule to the indicated subterm; running the tactic interpreter execute will cause the term to be converted to the form (?y + ?x) + ?z (which of course still has the same referent). The effect of the other special infix <= is to signal the intention of rewriting with the ``converse'' of the given theorem: if ASSOC is the theorem ((?x+?y)+?z)=?x+?y+?z2, the effect of executing the tactic interpreter on ASSOC <= ?a+?b+?c will be to convert the term to the form (?a+?b)+?c.
When there are several embedded theorems present, the tactic interpreter applies all of them, following a depth-first strategy (this needs to be qualified where expressions defined by cases are involved; see below). This applies as well to any embedded theorems which are introduced by rewriting with other theorems: it is possible to prove theorems which contain embedded theorems (though only on the right side). When an embedded theorem cannot be used to rewrite the subterm to which it is attached, it is simply dropped.
Further, it is possible to prove theorems which invoke recursive calls to themselves. It is necessary to use a special declaration command to do this, as we will see in the example below (since theorem names can be embedded in terms, they are required to be declared; the prove command normally serves to declare a theorem name, but this will not work when recursive dependencies are present; this is analogous to the treatment of forward declarations and function prototypes in programming languages).