next up previous
Next: Wednesday, January 26 Up: Lecture Notes Previous: Monday, January 24

Tuesday, Jan 25: Lab 1

Today we are doing the first lab with the Watson theorem prover.

The prover is installed on baron and packrat (and all of you now have
accounts on these systems).

To start the prover, start an X-terminal and enter the commands

cp /usr/local/public/holmes/*wat .

(this command will copy some files you need to your home directory)

mosml

(the Moscow ML interpreter comes up
the hyphen is the ML prompt)

- load "firstorder"; open firstorder;

(these commands start the prover)

- script "prop_equational";

(this command sets up a pre-packaged theory which we will work in)

Some useful facts:

Prover commands are usually issued at the ML prompt.  Commands begin
with a keyword (a function defined in Standard ML) followed by one or
more arguments.  Most arguments are enclosed in double quotes " ";
occasionally a numeral appears as an argument of a command without
quotes.  Commands with no argument have a dummy argument () (just a
pair of parentheses).  All ML commands end with a semicolon and it is
possible to put more than one command on a line.

If you make syntax errors, you will get error messages from ML; you can
usually ignore these messages and retype your command.  I have never known
an ML error to damage a prover session.

Every time ML executes a command, it reports a ``return value'' in
a line like this:

> val it = () : unit

These lines are just static so far as we are concerned.

Watson's view of the world is algebraic:  all Watson theorems are equations,
implicitly universally quantified over the variables appearing in them.

A brief overview of the Watson term language:

        atomic terms are strings of letters (Watson is case sensitive)
        numbers and the special characters ? and _.  
        
        A string of
        digits is a numeral (Watson incorporates arithmetic of non-negative
        integers of arbitrary length).  

        A string starting with ?
        and containing at least one non-digit in addition to the ?
        is a ``free variable'' (the only kind of variable we will see
        initially; usually we will use strings like ?x as free variables).

        An atomic term which is not a numeral and does not start with ?
        is a constant; constants have to be declared by the user in the
        course of development of a theory.  The only constants we will
        see are ``true'',  ``false'' and theorem names.

        Compund terms are built in three ways:  prefix operator terms,
        infix operator terms, and function terms.  Function terms
        are enclosed in brackets [ ] and usually contain ``bound variables''
        (terms consisting of ? followed by a numeral); we won't
        see any of these in this lab.

        Operators are strings of special characters other than ?,_
        quotes or paired forms (parentheses, braces and brackets).  The
        operators you will see in this lab are the propositional connectives
        (in typewriter form) and some special operators which will be
        introduced as we go along.  Declarations in a theory tell the
        prover whether operators are unary or binary (everything
        is predeclared for you in the lab).

        Terms involving operators can be disambiguated with parentheses.
        The default precedence convention of Watson is that all operators
        have the same precedence and group to the right; however, Watson
        allows user control of precedence and grouping, and the precedence
        has been set to go along with the conventions described in class.
        Remember that all operators group to the right rather than the left;
        this is probably the main difference from expectations.  Do not use
        brackets [ ] as an alternative to parentheses; the prover will
        accept terms with brackets, but they don't mean what you expect!
        You will find that you cannot use braces { } at all; the prover
        won't let you.

At this point you should have a theory on your desktop (the theory
``prop_equational'') if your setup commands worked.  We now start
introducing prover commands.

A Watson session is the proof of an equation.  The session starts with
a command which enters the intended left side of the equation to be proved
(though user commands can modify the left side of the equation during
the proof, they usually modify the right side).

- start "(?p & ?q) | (~?p & ?r)"; 

The ``start'' command, of which we see an example here, sets up an
equation of the form A = A (where A is the term we start with).  Further
user commands usually modify the right side of the equation being proved,
and what the user sees is usually the term on the right side of the equation.
What you should see at this point is this:

Global term display:

   {(?p & ?q) | ~ ?p & ?r}


Local term display:

   (?p & ?q) | ~ ?p & ?r

Notice that the rightmost set of parentheses you might expect is not
present; this is because the connectives & and | have the same precedence,
and the right grouping of connectives of the same precedence is enough
to determine what is meant:  the prover always displays as few parentheses
as possible.

The next set of commands we introduce are the movement commands ``right''
``left'' ``up'' and ``top''.

Try this sequence of commands:

- right();

Global term display:

   (?p & ?q) | {~ ?p & ?r}


Local term display:

   ~ ?p & ?r

(we don't give the display after the later commands)

- left();

- up();

- top();

- left();

- right();

- up();

- top();

You will see that these commands are used to navigate through the parse
tree of the term.  The Global term display:  prompt always shows the full
right side of the equation being proved, while the Local term display:
prompt shows a selected subterm of that term.  In the global display,
braces indicate the location of the selected term.

One thing you can use this feature for is clarification of the structure of
a term (if you are not sure of grouping).  If you make an illegal ``move''
using these commands you will get a ``Subterm error'' command, from
which you can recover using the top(); or up(); commands.

The main reason that we have the movement commands is to allow us to
control the application of algebraic rules (equations which are axioms
or previously proved theorems).  The commands we have available are
``ruleintro (ri)'', ``revruletintro (rri)'' and ``execute (ex)''.  The forms
in parentheses are abbreviations which can be used in place of the full
names of the commands.

- thmdisplay "COMMD";

   COMMD:  

   ?x | ?y   =

   ?y | ?x

   COMMD , 0

We have a theorem COMMD which expresses the commutative law of disjunction
(the last line of a theorem expresses the dependencies of the theorem on
axioms and definitions and can be ignored by us for now).

- ruleintro "COMMD";

Global term display:

   {COMMD => (?p & ?q) | ~ ?p & ?r}


Local term display:

   COMMD => (?p & ?q) | ~ ?p & ?r

This command introduces a label into the term telling us that we intend
to apply the theorem COMMD.  The special operator => (and another special
operator <=) indicate such ``embedded theorems''.  We carry out any such
announced theorem applications using the ``execute'' command.

- execute();

Global term display:

   {(~ ?p & ?r) | ?p & ?q}


Local term display:

   (~ ?p & ?r) | ?p & ?q

Now we demonstrate the use of the movement commands.

- left();

Global term display:

   {~ ?p & ?r} | ?p & ?q


Local term display:

   ~ ?p & ?r

- ri "COMMC"; ex();

Global term display:

   {COMMC => ~ ?p & ?r} | ?p & ?q


Local term display:

   COMMC => ~ ?p & ?r

> val it = () : unit
- 
Global term display:

   {?r & ~ ?p} | ?p & ?q


Local term display:

   ?r & ~ ?p

As we remarked above, we can put more than one command on the same line.
Notice that we used abbreviated forms of the names of the commands.
To illustrate the ``revruleintro'' command and to actually prove a little
theorem, we start a new proof:

- start "?p & ?q & ?r";

(we omit the display of the ``backed-up'' previous environment)

Global term display:

   {?p & ?q & ?r}


Local term display:

   ?p & ?q & ?r

- td "ASSOCC";


   ASSOCC:  

   (?x & ?y) & ?z   =

   ?x & ?y & ?z

   ASSOCC , 0

``td'' abbreviates ``thmdisplay''.   We are going to use this theorem to
rewrite a term of the form ?x & ?y & ?z to the form (?x & ?y) & ?z, rather
than _vice versa_.  The intention to apply a theorem in reverse is signalled
with the ``revruleintro (rri)'' command, and denoted in the term with the
<= reserved operator:

- rri "ASSOCC"; ex();     

Global term display:

   {ASSOCC <= ?p & ?q & ?r}


Local term display:

   ASSOCC <= ?p & ?q & ?r

> val it = () : unit
- 
Global term display:

   {(?p & ?q) & ?r}


Local term display:

   (?p & ?q) & ?r

- left();

Global term display:

   {?p & ?q} & ?r


Local term display:

   ?p & ?q

- ri "COMMC"; ex();

Global term display:

   {COMMC => ?p & ?q} & ?r


Local term display:

   COMMC => ?p & ?q

> val it = () : unit
- 
Global term display:

   {?q & ?p} & ?r


Local term display:

   ?q & ?p

- top(); ri "COMMC"; ex();

Global term display:

   {(?q & ?p) & ?r}


Local term display:

   (?q & ?p) & ?r

> val it = () : unit
- 
Global term display:

   {COMMC => (?q & ?p) & ?r}


Local term display:

   COMMC => (?q & ?p) & ?r

> val it = () : unit
- 
Global term display:

   {?r & ?q & ?p}


Local term display:

   ?r & ?q & ?p

Now we use the lookback() command to see the (unmodified)
left side of the equation to be proved:

- lookback();

Initial term display:

   ?p & ?q & ?r

and we prove a theorem:

- prove "REVERSEC";


   REVERSEC:  

   ?p & ?q & ?r   =

   ?r & ?q & ?p

   ASSOCC , COMMC , 0

We can use this theorem just as we used the axioms above:

- start "(?a|?b)&(?c|?d)&?d&?e"; 


   backup:  

   ?p & ?q & ?r   =

   ?r & ?q & ?p

   COMMC , ASSOCC , 0


Global term display:

   {(?a | ?b) & (?c | ?d) & ?d & ?e}


Local term display:

   (?a | ?b) & (?c | ?d) & ?d & ?e

- ruleintro "REVERSEC"; ex();

Global term display:

   {REVERSEC => (?a | ?b) & (?c | ?d) & ?d & ?e}


Local term display:

   REVERSEC => (?a | ?b) & (?c | ?d) & ?d & ?e

> val it = () : unit
- 
Global term display:

   {(?d & ?e) & (?c | ?d) & ?a | ?b}


Local term display:

   (?d & ?e) & (?c | ?d) & ?a | ?b

To understand the way the theorem was applied, remember that
conjunction groups to the right.

As our in-class exercise for today, we are going to start by
carrying out the reduction of ?p <+> ?q -> ?r <-> ?s to
CNF which caused us pain yesterday.

- start "(?p <+> ?q) -> (?r <-> ?s)";

We demonstrate a useful command.

- left();

Global term display:

   {?p <+> ?q} -> (?r <-> ?s)


Local term display:

   ?p <+> ?q

> val it = () : unit
- srt();


   COMP:  

   (?f @@ ?g) @ ?x   =

   ?f @ ?g @ ?x

   COMP , 0




   FNDIST:  

   ?f @ ?x || ?y , ?z   =

   ?x || (?f @ ?y) , ?f @ ?z

   FNDIST , 0




   XOR:  

   ?p <+> ?q   =

   ?p || (?q || false , true) , ?q || true , false

   XOR , 0




   XOR_DEF:  

   ?x <+> ?y   =

   ~ (?x <-> ?y)

   XOR_DEF , 0

q
> val it = () : unit
-

The srt() command (short for ``show relevant theorems'') shows theorems
which you can apply (either in the usual sense or in the reverse sense)
to the selected theorem.  It is one of the devices you can use to find
out the names of theorems which you expect to exist and don't know the
names of.  Use ``q'' to break out when you have found the theorem you
want.  Notice that XOR_DEF is the theorem we'll want to apply here.
(XOR is rather mysterious -- we'll see it in a later lab).

We will illustrate another command useful for this purpose:

- top();

Global term display:

   {(?p <+> ?q) -> (?r <-> ?s)}


Local term display:

   (?p <+> ?q) -> (?r <-> ?s)

This should reduce (using the definition of ->) to 
the term ~(?p<+>?q)|(?r<->?s).

We issue a command

- tri "~(?p<+>?q)|(?r<->?s)";

Global term display:

   {IF_DEF => (?p <+> ?q) -> (?r <-> ?s)}


Local term display:

   IF_DEF => (?p <+> ?q) -> (?r <-> ?s)

The name ``tri'' abbreviates ``targetruleintro''; the argument of
the command is a target form that we want the term to take, and the
prover searches for  a theorem that will take us to that form if it
can find one.

- execute();

Global term display:

   {~ (?p <+> ?q) | (?r <-> ?s)}


Local term display:

   ~ (?p <+> ?q) | (?r <-> ?s)

Armed with this much, we will try to get to the CNF!  There will
be a problem with the application of the double negation theorem, which
I will discuss in class (it doesn't take quite the form one expects).



Randall Holmes
2000-05-05