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+?z`^{2}, 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).