CSE150 LECTURE NOTES

December 1, 2004
 
 

ANNOUNCEMENTS

(1) Doug's section for Friday will be Thursday instead, at 2pm in Center Hall room 218.

(2) Assignment 4  is due on Friday at 5pm.  You may include your report as a PDF file in your electronic submission, or you can slip it under the door of my office, which is APM 4856. 

(3) The final exam is next Monday, December 6, from 7pm to 10pm, in this room.

(4) Score reporting is up on WebCT.  Look for Assignment 3 scores Thursday evening.


RESOLUTION AND "MODUS PONENS"

Resolution is a single inference rule that, when used in the right way, yields an inference algorithm that is complete.  Resolution was invented by John Alan Robinson in 1965, building on ideas developed in the previous decade in the U.S. and in the Soviet Union.

So-called modus ponens is a very special case of resolution.  Suppose that p and q are the same literal, excpet that q is negated.  Then we have the inference rule.

 p    ~q v r
------------
       r
The modus ponens special case illustrates how resolution can make progress by yielding a conclusion that is shorter than its antecedents.  In general, resolution yields a conclusion that is longer than either of the two inputs

Usually, the literals p and q will not match exactly.  We may need to match a variable in one with a constant in the other.  This process is called unification; see later. 


REFUTATION PROOFS

Let's look at a theorem-proving method for FOL.  This is basically the method used by Otter.

In order to prove a sentence in first-order logic, say alpha, add the negation of alpha to the knowledge base and derive a contradiction, i.e. prove that "false" follows from the axioms in the knowledge base.  We're using the fact that KB |= alpha if and only if KB union { ~alpha } |= false.

Example: How to prove eats(jo,fish) from the following axioms?  (Here x, y, z are variables that are implicitly universally quantified.)

~cat(x) v likes(x,fish)
~cat(y) v ~likes(y,z) v eats(y,z)
cat(jo)
Answer: add ~eats(jo,fish) and derive ~beta and beta separately for some literal beta.  For example:

    ~eats(jo,fish)     ~cat(y) v ~likes(y,z) v eats(y,z)
           \\            /
       ~cat(jo) v ~likes(jo,fish)    cat(jo)
                         \\         /
~cat(x) v likes(x,fish)  ~likes(jo,fish)
                    \      //
                     ~cat(jo)    cat(jo)
                           \     /
                             false

The proof above is typical, although of course it is very small.  Some typical aspects:

The "backbone" or main path of the proof is indicated with double red slashes above.
 
 

RESOLUTION IN GENERAL

Exactly what inference rule(s) did we use in the example proof above?  Answer: Just one rule, named resolution.

Suppose that positive literal pj and the negative literal qk match each other.   Then

    p1 v ... v pj v ... v pm          q1 v ... qk v ... v qn
---------------------------------------------------------------
p1 v ... pj-1 v pj+1 ... v pm v q1 v ... qk-1 v qk+1 v ... v qn
In words, the consequent of the resolution inference rule is the disjunction of the two antecedent clauses, with the unifying literals pj and qk removed.

Resolution is a form of reasoning by cases: pj is either true or false (after unification).  If pj is true, then qk is false, so one of q1 v ... qk-1 v qk+1 v ... v qn must be true.  If  pj is false, then one of p1 v ... pj-1 v pj+1 ... v pm must be true.  Putting the either-or back together, one of the following must be true:  p1 v ... pj-1 v pj+1 ... v pm v q1 v ... qk-1 v qk+1 v ... v qn.

Resolution is a generalization of modus ponens, and also of unit propagation, which we saw as part of the DPLL algorithm.

As with modus ponens, usually the literals pj and qk will not match exactly.  We may need to match a variable in one clause with a constant in the other.  This process is called unification; see later. 

 

COMPLETENESS OF RESOLUTION

Definition: The proof algorithm |- is refutation-complete if whenever KB |= A then KB union { ~A} |- false eventually, in finite time.

Theorem: Resolution is refutation-complete.

This theorem says that if KB entails A, then resolution will demonstrate this fact eventually.   Of course, resolution is sound also, which is even more important than completeness!

As stressed before, if A is not entailed by KB then resolution applied to KB union {~A} may fail to terminate.

It is possible that neither A nor ~A is entailed by KB.  In this case it is possible to get non-termination from KB union {~A} and from KB union {A}.


CLAUSAL NORMAL FORM

In order to apply resolution, sentences of FOL must first be converted into clausal normal form (CNF, also called conjunctive normal form).  Definition: A CNF sentence is a universally quantified disjunction ("or") of literals.  A literal is a positive or negative atom.  An atom is a predicate with its arguments, i.e. a primitive true/false sentence.

To translate into CNF, connectives other than "or" are eliminated by de Morgan's laws, associativity, and distributivity.  Existential quantifiers are eliminated by Skolemization, which introduces new constants and/or function symbols.  For example,

forall x exists y loves(x,y)
becomes
forall x loves(x,objectof(x))
The Skolem term objectof(x) that replaces y has x as an argument because the scope of y is nested inside the scope of x.
 
 

UNIFICATION

When two clauses in FOL are resolved together, we may need to match a variable in one clause with a constant in the other.  This process is called unification.  The result of unification is a substitution, i.e. a set of bindings, where each binding is an association between a variable and a term.  For example, consider these two CNF clauses in FOL:
forall x   loves(x,mother(x))
forall y,z loves(y,z) -> likes(y,z)
The substitution that unifies the two  loves  literals is a set of two bindings: { y := x, z := mother(x) }

After applying the substitution to both clauses, we can then conclude by resolution that

forall x likes(x,mother(x))