The basic session model of Watson

A typical Watson session begins with a user entering a term. The user then manipulates the term by applying theorems to subterms of this term as rewrite rules (all Watson theorems are equations), and closes by proving a theorem to the effect that the term originally entered is equal to the term finally arrived at.

There are two moves available to the user which qualify this picture: he may interchange the term originally entered and the term most recently arrived at, or he may carry out a global substitution of some term for a free variable, which will affect the term originally entered as well as the term most recently arrived at.

Though it appears to the user that he is ``editing'' a term, what he is actually editing is an equation. Internally, the prover stores two terms, the left side and right side of the equation being edited. What the user views is the right side of the equation (there is also a command available to view the left side). There is a command which interchanges the left and right sides of the equation, and there is a global assignment command which replaces a free variable by the same term everywhere in the equation; all other commands manipulate the right side only. At the end of the session, the user proves the current equation: he assigns a name to it and it is stored as a new rewrite rule available for the proof of further theorems.

We reproduce the rules of equational reasoning from above and point out how they are implemented in the basic session model:

reflexivity:

A = A is an axiom for any term A.

Each such axiom is implemented by simply entering the term A (which has the effect of making the current equation A = A).

symmetry:

if A = B is a theorem, then B = A is a theorem.

If A = B has been proved, the user can swap the left and right hand sides of the theorem to prove B = A.

transitivity:

if A = B is a theorem and B = C is a theorem, then A = C is a theorem.

A sequence of rewrites which prove A = B, followed by a sequence of rewrites which prove B = C, give a proof of A = C.

We recall the notation A[T/x] for the result of substituting the term T for the free variable x in the term A. If T is a term containing bound variables (or ``embedded local hypotheses'', a topic to be discussed below), there are some technicalities to be considered below in how the substitution is effected.

substitution:

if A = B is a theorem, then C[A/x] = C[B/x] is a theorem.

This is implemented by the ability to apply the theorem A = B as as a rewrite rule, possibly repeatedly (how this is done is described in more detail in the next subsection).

generality:

if A = B is a theorem, then A[C/x] = B[C/x] is a theorem.

This is implemented by the global assignment command.