next up previous
Next: Tuesday, February 1 Up: Lecture Notes Previous: Friday, January 28

Monday, January 31 (Lab 2)

Notes for Monday, January 31 (Lab 2):

On Monday afternoon, I put the files definition.wat and prop_equational.wat,
which are needed for labs 1 and 2, on my web page with the other
Watson scripts (follow the link from my main page to the prover, and from
the prover page to the Watson scripts).  I will maintain these files
both in the /usr/local/public/holmes directories on baron and packrat
and on my web page.

I reproduce the list of axioms for Boolean algebra from above
with names for the axioms as theorems in the preloaded Watson theory,
for reference.

double negation (DNEG):

~~X == |- X

commutative laws (COMMC, COMMD):

X & Y == Y & X                      X | Y == Y | X

associative laws (ASSOCC, ASSOCD):

(X & Y) & Z == X & (Y & Z)          (X | Y) | Z == X | (Y | Z)

distributive laws (DISTC, DISTD):

X & (Y | Z) == (X & Y) | (X & Z)    X | (Y & Z) == (X | Y) & (X | Z) 

idempotent laws (IDEMC, IDEMD):

X & X == |- X                          X | X == |- X

cancellation laws (CANCELC, CANCELD):

X & ~X == false                     X | ~X == true

identity laws (IDC, IDD):

X & true == |- X                       X | false == |- X

zero laws (ZERC, ZERD):

X & false == false                  X | true == true

deMorgan laws (DEMC, DEMD):

~(X & Y) == ~X | ~Y                 ~(X | Y) == ~X & ~Y

In the statement of the double negation, identity, and idempotent laws
a new symbol |- appears.  This is a unary ``assertion'' operator.  |-
?x is intended to mean ``true'' if ?x is equal to ``true'' and
``false'' if ?x is equal to anything else (the point being that there
are objects other than truth values in the universe).  |- has the same
precedence as negation (it binds more tightly than anything else).  To
manage the |- symbol we have the following theorems:

ASSERTS:  |- ?x == |- |- ?x

NRULE1:  ~?x == |- ~ ?x

NRULE2:  ~?x == ~ |- ?x

CRULE1, DRULE1:  ?x & ?y == |- (?x & ?y)   ?x | ?y == |- (?x | ?y)

CRULE2, DRULE2:  ?x & ?y == |- ?x & ?y     ?x | ?y == |- ?x | ?y

CRULE3, DRULE3:  ?x & ?y == ?x & |- ?y     ?x | ?y == ?x | |- ?y

Also, theorems defining some additional operators:

IF_DEF:  ?p -> ?q == ~ ?p | ?q

IFF_DEF:  ?p <-> ?q == (?p -> ?q) & (?q -> ?p)

XOR_DEF:  ?p <+> ?q == ~ ?p <-> ?q 

These theorems are all given in forms which introduce new occurrences
of |-; they can be used in reverse to get rid of occurrences of |-, which
is what one usually wants to do.  One needs to introduce new occurrences of
|- only if one is going to apply one of the theorems involving |- (double
negation, identity, and idempotent laws) in reverse, which happens less
often than a |- symbol being introduced by application of one of these laws.

There is also a useful piece of automation in the file prop_equational.wat:
there is a ``theorem'' CLEANUP (actually a little program) which will get
rid of all unwanted occurrences of |-.  We will talk about how programs like
CLEANUP are developed in a later lab.

The best way of thinking of |- is as a ``type label'' telling us that a term
is a truth value.  In most contexts in propositional logic this ``type label''
can be eliminated because one can tell from context that the formula
is intended to stand for a truth value; the only context where we can't
eliminate it is where it stands in front of an isolated propositional letter
(and even then we can get rid of it if the isolated letter is part of a larger
formula).  |- is a technicality which I don't need you to spend too much
time thinking about (this is why I added the automatic procedure to get
rid of it!).

Distributivity on the other side is provided as DISTC2 and DISTD2.

In the lab we will work together on putting the term

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

into CNF (the example we did in class).

We did this in class; within the next day or so I'll try to put the full
account of what we did here in the notes.

Logistics of doing exercises:

It is a good idea to develop an editor file of prover commands in 
emacs or vi, edit your computer proofs in the editor window and ``drag
and click'' to execute them on the prover.  You can then send me the final
version of your editor file.

The prover does have a scripting feature.  If you type 

makescript "NAME";

the prover will put you into its internal shell (which looks very much
like the shell you have been working in, but has different prompts).
Your commands are then stored in a file called NAME.log.wat.  You
leave the internal shell by typing quit(); this will put you back in
the ML interpreter.  You can view the script file NAME.log.wat with an
editor (it is just an ASCII file).  I will accept scripts or other
files of prover commands describing your work on the exercises in
fulfilment of the lab assignment.  They should be mailed to me at
holmes@math.boisestate.edu (I prefer plain ASCII files to files with
MIME attachments, but I can deal with the latter).  Completed lab
files are due by Monday, February 7.

Another useful tidbit:  you can use the command

saveenv "name_of_session";  

(where name_of_session can be any name
you want to assign to your session) to save a proof at a certain stage.
The command 

getenv "name_of_session";

will restore the proof to its status when it was saved.  This can
be handy, as not all proof steps are reversible and even when they are
it can be hard to see how to get back to an earlier stage.

Yet another useful tidbit:

If you have created a script test.log.wat using the
command 

- makescript "test";

you can run this script using the command

- script "test.log";

If you have made this script and ended your session and want to continue
work based on the same script, do not issue

makescript "test";

again; this will erase your file!  Instead, do something like this:

- makescript "test2";

Watson> script "test.log";

This will cause the prover to run the old script as the first command
on the new script test2.log.wat.  If you record your work this way,
you will need to send all scripts that you generate to me.  I don't
mind receiving several files!

I don't necessarily recommend this approach; I think it is a better idea
to use an editor and create your own script file and rerun it as necessary
using the ``drag-and-click'' features of the operating system.  But this
did come up in  conversation with a student, so I thought I'd make it
available.

EXERCISES:  

Verify that ?p->?q|?p is a tautology; 

Verify that
(?p->?q)<->(~?q -> ~?p) is a tautology (contrapositive);

Show that ((?p->?q)&(?q->?r))->(?p->?r) is a tautology (this may be
harder).  HINT (added Feb. 4): convert it to CNF: then it will be easy
to see that it has to be true.  I also added more parentheses Feb 4.

In this first batch of exercises, the objective is to show that
the formula given is equal to the formula ``true''.

MORE EXERCISES: convert ?x <+> ?y to DNF; convert ?x <-> ?y to CNF (this
is easy!); convert ?p<->?q<->?r to CNF.



Randall Holmes
2000-05-05