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.