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).