CSE 250A Lecture Notes, February 26, 2001

CSE 250A LECTURE NOTES

February 26, 2001

ANNOUNCEMENTS

I'm distributing the description of the fourth and last project. This involves knowledge representation and reasoning in first-order logic.

Next quarter Prof. Victor Vianu will teach a graduate course, CSE 208D, on Logic in Computer Science. Highly recommended!

PLANNING PROBLEMS

Given information about the initial state, the planning task is to discover a sequence of actions such that certain fluents hold in the final state. Example: find P such that

T & holds(alive,s_0) |= holds(dead,P).

The answer is P = do(do(do(s_0,load),wait),shoot)

Solving a planning problem requires a logical reasoning system (i.e. a knowledge base manager or inference engine) that can return existential witnesses in addition to saying (yes, no, or unknown) whether or not a certain sentence is entailed by a given knowledge base.

Unfortunately, doing planning by general-purpose logical reasoning is just not efficient computationally.

The most successful planners today operate by translating a first-order knowledge base into propositional 3SAT clauses, then running a local search algorithm like WalkSat.

REFUTATION PROOFS

In order to prove a sentence in first-order logic 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.

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 same axiom may be used many times, e.g. cat(jo) above.
The first step in the proof uses the negated goal.
The proof has a linear structure: each step uses the conclusion of the previous step, together with an axiom.

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

RESOLUTION

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

Resolution is a single inference rule that, when used in the right way, yields an inference algorithm that is complete. Resolution was invented by J. A. Robinson in 1965, building on ideas developed in the previous decade in the U.S. and in the Soviet Union. You have seen resolution for propositional logic in previous classes. Here we look at the first-order case, and at control strategies.

Suppose that positive literal pj and the negative literal qk can be unified, with substitution S (to be explained later). 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)S

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, and the unifying substitution S applied.

So-called modus ponens is a very special case of resolution. Let j = m = 1 and k = 1, n = 2, and show the negation sign on q1:

p1 ~q1 v q2
--------------
(q2)S

The modus ponens special case illustrates how resolution can make progress by yielding a conclusion that is shorter than its antecedents.

Resolution is a form of reasoning by cases: either pj is true, or qk is true, after unification; there is no third possibility.

REFUTATION PROOFS AND CONJUNCTIVE NORMAL FORM

Lemma: KB |= alpha if and only if KB union { ~alpha } is unsatisfiable.

Theorem: Resolution is sound and refutation-complete, meaning that if a set of sentences is unsatisfiable, then resolution will derive a contradiction.

In order to apply resolution, sentences of FOL must first be converted into conjunctive normal form (CNF).

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.