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.