next up previous
Next: Monday, February 28 Up: Lecture Notes Previous: Tuesday, February 22 and

Friday, February 25 - Lab 3

Announcement: If you see this, all versions of the prover have been updated to allow the ``stepsnorules'' command and to correct the bug in user-defined precedence (I hope - keep me posted if it parses any terms strangely!). If you are running the prover on a home machine, you should download the latest version of the ``draft'' source from the web page. To check correctness of version, run

- versiondate();

You should get a February 25 date.

Lab 3, February 25.  Exercises due Friday, March 3.

This lab contains a demonstration component (some stuff we will do
together) and then some fairly simple stuff for you to do based on
Grantham's section 5.4.

First, I will demonstrate the ``programming'' component of the
prover.  You may have wondered why the prover requires the introduction
of ``labels'' for each theorem applied (using ``ri'' or ``rri'')
before applying the theorem with ``ex''.

Set up the prover by issuing the following commands:

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

(this refreshes your script files)

mosml

(this starts the ML interpreter)

load "firstorder"; open firstorder;

(this starts the prover)

script "lab3";

(this sets up the preloaded stuff for this lab, which
includes everything from Lab 2)

GENERAL HINT:  the lab is visible as the Feb. 25 notes in Netscape;
you might want to open a Netscape window and get the example commands
from the Netscape window to the xterm window; this will save typing!

``Programming'' under Watson

This section of the lab is a demonstration.  There is an optional
exercise at the end.  It is useful to understand this section because it
will probably be the subject of a (paper-and-pencil) proof by structural
induction later in the course.

We look at a familiar theorem:

- td "ASSOCC";


   ASSOCC:  

   (?x & ?y) & ?z   =

   ?x & ?y & ?z

   ASSOCC , 0

(this is simply the associative law of conjunction)

We will prove a ``theorem'' which will act as a program to convert
any conjunction to a completely right-associated form (with no visible
parentheses).

- dpt "A1";

This command tells the prover that A1 is the name of a theorem without
telling it what the theorem is.  dpt abbreviates
``declarepretheorem'', for what that's worth.

- s "(?x & ?y) & ?z";

Global term display:

   {(?x & ?y) & ?z}


Local term display:

   (?x & ?y) & ?z

(We enter a term identical to the left side of the theorem
ASSOCC.)

- ri "ASSOCC"; ex();

Global term display:

   {ASSOCC => (?x & ?y) & ?z}


Local term display:

   ASSOCC => (?x & ?y) & ?z
 
Global term display:

   {?x & ?y & ?z}


Local term display:

   ?x & ?y & ?z

(We introduce an application of the theorem ASSOCC and carry it out)

- ri "A1";

Global term display:

   {A1 => ?x & ?y & ?z}


Local term display:

   A1 => ?x & ?y & ?z

(We introduce an application of the as yet undefined theorem A1???)

- prove "A1";


   A1:  

   (?x & ?y) & ?z   =

   A1 => ?x & ?y & ?z

   ASSOCC , 0

(And we prove A1 in a form which mentions A1.  Something fishy is 
going on here...)


To see what is happening, we need to apply the ``theorem'' A1 to
an example:

- s "((?x&?y&?z)&?u&?v&(?w&?x)&?y)&?z&?a";


Global term display:

   {((?x & ?y & ?z) & ?u & ?v & (?w & ?x) & ?y) & ?z 
         & ?a}


Local term display:

   ((?x & ?y & ?z) & ?u & ?v & (?w & ?x) & ?y) & ?z & ?a

- ri "A1"; ex();

Global term display:

   {?x & (?y & ?z) & (?u & ?v & (?w & ?x) & ?y) & ?z 
            & ?a}


Local term display:

   ?x & (?y & ?z) & (?u & ?v & (?w & ?x) & ?y) & ?z & ?a

(This eliminated a lot of parentheses, but not all of them).

Another pass at this:


- startover();

Global term display:

   {((?x & ?y & ?z) & ?u & ?v & (?w & ?x) & ?y) & ?z 
         & ?a}


Local term display:

   ((?x & ?y & ?z) & ?u & ?v & (?w & ?x) & ?y) & ?z & ?a

(startover is a handy command; it takes you back to the 
state you started the current proof in, unless you have made
global assignments to variables).

- ri "A1"; steps();  (after this hit Enter repeatedly)

   A1 => ((?x & ?y & ?z) & ?u & ?v & (?w & ?x) & ?y) 
   & ?z & ?a

   A1 => (?x & ?y & ?z) & (?u & ?v & (?w & ?x) & ?y) 
      & ?z & ?a

   A1 => ?x & (?y & ?z) & (?u & ?v & (?w & ?x) & ?y) 
      & ?z & ?a

   ?x & (?y & ?z) & (?u & ?v & (?w & ?x) & ?y) & ?z & ?a

(in the interests of saving paper, I edited the display 
considerably.  steps is a trace command; it advances one step
each time you hit Enter; you can break out by hitting q instead.)

The execution of the trace command ``steps'' shows us what happens.
Application of the ``theorem'' A1 introduces new occurrences of A1,
which are themselves carried out in their turn.  The ``theorem'' A1 is
true because the term A1 => ?x + ?y + ?z has the same value as ?x + ?y
+ ?z; the ``A1 => ...'' is just an annotation.  But the annotated term
has very different ``execution behavior''!

A1 is a recursive program; it works by invoking itself.  As with any
looping or recursion, it is important to see that you will be able to
get out:  the escape hatch lies in the fact that in  

A1 => ?x & (?y & ?z) & (?u & ?v & (?w & ?x) & ?y) 
      & ?z & ?a

the target term doesn't match the left side of the theorem A1; in this
case the embedded theorem application is simply dropped and the process
stops.  It is perfectly possible to write programs which do go into infinite
loops in Watson!

If you think about it, you should be able to see that A1 removes all
_leading_ parentheses in a conjunction.  I promised you a program which
would remove _all_ parentheses from a conjunction:  here it comes!

- dpt "A2";  
 
- s "?x & ?y";

Global term display:

   {?x & ?y}


Local term display:

   ?x & ?y

- ri "A1";     

Global term display:

   {A1 => ?x & ?y}


Local term display:

   A1 => ?x & ?y

- ri "RIGHT@A2";

Global term display:

   {(RIGHT @ A2) => A1 => ?x & ?y}


Local term display:

   (RIGHT @ A2) => A1 => ?x & ?y

- prove "A2";


   A2:  

   ?x & ?y   =

   (RIGHT @ A2) => A1 => ?x & ?y

   0

(This is an interesting ``proof'' because we actually haven't done
anything:  we propose to remove all leading parentheses from the
conjunction ?x & ?y then apply the same procedure recursively to
the right subterm).

Let's see how it works:

- s "((?x&?y&?z)&?u&?v&(?w&?x)&?y)&?z&?a";

- ri "A2"; ex();

Global term display:

   {?x & ?y & ?z & ?u & ?v & ?w & ?x & ?y & ?z & ?a}


Local term display:

   ?x & ?y & ?z & ?u & ?v & ?w & ?x & ?y & ?z & ?a

Wow!

You might want to try the following command lines:

- startover();

- ri "A2"; steps();  (Hit Enter repeatedly)

and for a slightly different effect
- startover();

- ri "A2"; stepsnorules();  (Hit Enter repeatedly)

Optional exercise 1:  How would you prove that this procedure works?
I'm not looking for a formalized proof, just a convincing argument.

Optional exercise 2:  Develop a ``theorem'' alias recursive program
which, when applied to any disjunction containing a disjunct of the
form ``true'' will convert the whole disjunction to ``true''.  It's
no fair using the EVERYWHERE tactic (this will work!); it is a good
idea to prove the easy theorem ZERD2 which says true|?x = true to
go along with the theorem ZERD: ?x|true = ?x which you already have.

Expressions Defined By Cases:  A Brief Introduction

An important special notation in Watson is

?x || ?y , ?z

which means ``if ?x is true, then ?y, else ?z''; it is a notation for
the idea of ``definition by cases'' which you have encountered in calculus.
The built-in logic of Watson relies heavily on special properties of 
expressions defined by cases:  in fact, it defines all propositional
connectives using this construction and uses properties of this construction
to derive all the properties of the propositional connectives.

We will briefly demonstrate some of the special properties of
expressions defined by cases which are involved (so that you will
have some understanding of why the very powerful automation in the
next section works).

In a term 

(?a = ?b) || T , U

I claim I should be able to replace any occurrence of ?a with
?b or vice versa inside the term T.

- s "(?a=?b)||(?a&?b&?c),?d";

Global term display:

   {(?a = ?b) || ?a & ?b & ?c , ?d}


Local term display:

   (?a = ?b) || ?a & ?b & ?c , ?d

(& binds more tightly than || or , 
so it doesn't need the parentheses I put in.)

- right();left();

Global term display:

   (?a = ?b) || {?a & ?b & ?c} , ?d


Local term display:

   ?a & ?b & ?c

- lookhyps();
1 (positive):  

   ?a  =  

   ?b

What this mysterious command tells me is that I can assume 
in this local context that ?a = ?b, and that this local hypothesis
is numbered 1.

- left();

Global term display:

   (?a = ?b) || {?a} & ?b & ?c , ?d


Local term display:

   ?a

- ri "0|-|1"; ex();

Global term display:

   (?a = ?b) || {?b} & ?b & ?c , ?d


Local term display:

   ?b

(the ``theorem'' 0|-|1 is a way of using hypothesis 1;
if I were using hypothesis 2 (if I were in a nested case
expression) I'd also have 0|-|2 handy.  The initial 0
tells me _how_ I'm using the hypothesis; there is also
a ``theorem'' 1|-|1 which we will see used.)

- rri "0|-|1"; ex();

Global term display:

   (?a = ?b) || {?a} & ?b & ?c , ?d


Local term display:

   ?a

(we can also use the local theorem ?a = ?b in reverse to convert ?b to ?a)

- s "(?a=?b)||?X,?Y";
- assign "?X" "(?a=?b)||0,1";
- assign "?Y" "(?a=?b)||2,3";

Global term display:

   {(?a = ?b) || ((?a = ?b) || 0 , 1) , (?a = ?b) || 2 
               , 3}


Local term display:

   (?a = ?b) || ((?a = ?b) || 0 , 1) , (?a = ?b) || 2 
            , 3

(I omit intermediate displays.  This use of the ``assign''
command (which makes global assignments to variables throughout
the equation being proved) to build complex terms will be seen in
the last part of the lab.

I claim that the inner occurrences of ?a=?b are both redundant.
See if you can figure out for yourselves how this expression can
be simplified.

Now we do it:

- right(); left(); ri "1|-|1"; ex();

Global term display:

   (?a = ?b) || {0} , (?a = ?b) || 2 , 3


Local term display:

   0

- top(); right(); right(); ri "1|-|1"; ex();

Global term display:

   (?a = ?b) || 0 , {3}


Local term display:

   3

In each case, I only show the final display.  Run this command:

- lookhyps();
1 (negative):  

   ?a  =  

   ?b

Note that the prover knows that you are in the negative branch of the
case expression.

You can also ``undo'' the 1|-|1 command:

- rri "1|-|1"; ex();

Global term display:

   (?a = ?b) || 0 , {(?a = ?b) || ?x_228 , 3}


Local term display:

   (?a = ?b) || ?x_228 , 3

(You will probably not get the same new variable I got; the
point is that no matter what you put there, this is the same as
the previous term).

The 1|-1 (and 1|-|2, 1|-|3, etc) tactics for eliminating redundant
hypotheses for case expressions are the driving force behind a complete
tautology checker TAUT, which we will use in the next section.

A final point:  if you issue the commands

- compress(); statementdisplay();

you will get a more compact presentation (vertically -- fewer
returns) and a more economical presentation of the output of the
``lookhyps'' command in the next section.  ``compress'' is reversed by
``expand'' and ``statementdisplay'' is a toggle:  if you like the old
display better you can type

- expand(); statementdisplay();

Propositional Logic Via Case Expressions; Simplifying Proof Trees
     Using Watson

Each of the propositional connectives has a definition in terms of
the logic of case expressions, given in definitions.wat.  For example,

- td "AND";


   AND:  

   ?p & ?q   =

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

   AND , 0

This tells us that if ?p and ?q are both equal to true we will get the
value true, and in any other case we will get false, which should 
square with our understanding of the meaning of &.

I suggest these commands:

- td "OR";

- td "IF";

- td "NOT";

Display the definitions and see if you believe them.

Using these definitions and the 1|-|n tactics introduced in the previous
section, and the programming techniques introduced in the first section,
I wrote a ``theorem'' called TAUT which converts any tautology to 
true and converts any other propositional expression to an (admittedly
not very easy to read) case expression format, formally similar to 
Grantham's ``proof trees'' (which have a much better GUI).  Despair
not:  I provide a very tricky tactic called CASE_VIEWER and a relative
called COUNTER_VIEWER which will allow you to extract information from
these complicated case expressions.

My lab example is problem 7 from section 5.4 in Grantham's book.

The setup I show is a model for how to do it; you need to compare
with Grantham's text:

- s "?P1 & ?P2 & ?P3 & ?P4 -> ?Conc";

Global term display:

   {?P1 & ?P2 & ?P3 & ?P4 -> ?Conc}


Local term display:

   ?P1 & ?P2 & ?P3 & ?P4 -> ?Conc

(we use the assign command illustrated above to fill in the premises
and the conclusion)

- assign "?P1" "?A -> (?B & ?C)";
- assign "?P2" "?B -> (?D | ?Q)";
- assign "?P3" "?C -> (?Q -> ?R)";
- assign "?P4" "?D -> (~?A <-> ?B)";

Global term display:

   {(?A -> ?B & ?C) & (?B -> ?D | ?Q) & (?C -> ?Q -> ?R) 
            & (?D -> (~ ?A <-> ?B)) -> ?Conc}


Local term display:

   (?A -> ?B & ?C) & (?B -> ?D | ?Q) & (?C -> ?Q -> ?R) 
         & (?D -> (~ ?A <-> ?B)) -> ?Conc

We don't want to repeat this with the second conclusion, so we
save the current state of the proof:

- saveenv "premises";

   premises:  

   (?A -> ?B & ?C) & (?B -> ?D | ?Q) & (?C -> ?Q -> ?R) 
         & (?D -> (~ ?A <-> ?B)) -> ?Conc   =

   (?A -> ?B & ?C) & (?B -> ?D | ?Q) & (?C -> ?Q -> ?R) 
         & (?D -> (~ ?A <-> ?B)) -> ?Conc

   0

(We'll see how to retrieve this later)

Now we do the first conclusion:

- assign "?Conc" "?A -> ?R";

Global term display:

   {(?A -> ?B & ?C) & (?B -> ?D | ?Q) & (?C -> ?Q -> ?R) 
            & (?D -> (~ ?A <-> ?B)) -> ?A -> ?R}


Local term display:

   (?A -> ?B & ?C) & (?B -> ?D | ?Q) & (?C -> ?Q -> ?R) 
         & (?D -> (~ ?A <-> ?B)) -> ?A -> ?R

Here's the complete setup; it is not reasonable to expect to
be able to type this directly at the ML interface!

- ri "TAUT"; ex();

(this takes a little while; TAUT is not very fast)

Global term display:

   {true}


Local term display:

   true

Wow!

Now let's try the other conclusion:

- getenv "premises";

Global term display:

   {(?A -> ?B & ?C) & (?B -> ?D | ?Q) & (?C -> ?Q -> ?R) 
            & (?D -> (~ ?A <-> ?B)) -> ?Conc}


Local term display:

   (?A -> ?B & ?C) & (?B -> ?D | ?Q) & (?C -> ?Q -> ?R) 
         & (?D -> (~ ?A <-> ?B)) -> ?Conc

(this restores that saved state)

- assign "?Conc" "?B&?C->?R";

- ri "TAUT"; ex();

Global term display:

   {?A || true , ?B || (?D || (?C || (?Q || true , ?R 
               || true , false) , true) , true) , true}


Local term display:

   ?A || true , ?B || (?D || (?C || (?Q || true , ?R 
            || true , false) , true) , true) , true

You should be able to see that this is an expression defined by
cases, and in all but one of these cases, it is true.

A manual approach, which I ask you to take, is to use the right
and left commands to navigate to the occurrence of ``false''
and then issue the command

- lookhyps();

You will see a description of a situation which makes the conclusion
false while the premises are true!

If you are lazier, you should like the results of this better:

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

You will find yourself looking at a subterm of the form either
``true'' or ``false'' and some information about local hypotheses.
At the

INPUT:

prompt type ``next'' and hit Enter.  Repeat until it stops.

You got a look at all the cases, including the counterexample.

Now try COUNTER_VIEWER:

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

This takes you right where you want to be.  next will take you out,
or to the next counterexample in a more complicated example.

Exercise (mandatory):  Do three of problems 5-26 in section 5.4
of Grantham (photocopies of these pages supplied).  At least one
of these should have more than one conclusion (and you should do
each).  Determine in each case whether the conclusion follows from
the premises; if not, extract a description of the counterexamples
from the Watson output.  You need to do at least one problem where you
get a tautology and at least one where you extract a counterexample
(so you may end up doing extras if you are unlucky).  Problem 7 is
of course not available.

You will need to write some English in describing the counterexamples
in invalid proofs; just write it into the computer file you send me.



Randall Holmes
2000-05-05