CSE 250A Lecture Notes, March 5, 2001

CSE 250A LECTURE NOTES

March 5, 2001

ANNOUNCEMENTS

The topic for the last three lectures of the quarter will be knowledge representation using probability theory. This is important background for understanding many modern learning algorithms. Today's topic is the efficient use of resolution for proving theorems in first-order logic.

I have received no questions about the fourth project, either directly or on the discussion board. I find it hard to believe that everything is crystal clear and that Otter is so easy to use.

CONJUNCTIVE NORMAL FORM

In order to apply resolution, sentences of FOL must first be converted into conjunctive normal form (CNF). Reminder: 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))

In general, a substitution S is a set of individual substitutions of the form x := g where x is a variable and g is a term. Each righthand side term may be ground (i.e. containing no variables) or not.

Applying the substitution S is usually written using postfix notation. The equation pS = qS says that after applying S to p and to q, the results are syntactically identical. Terminology: we say that S unifies p and q, or that S is a unifying substitution for p and q.

There is a standard algorithm that given two sentences, finds their unique most general unifying substitution. Notes:

A variable cannot be replaced by a term containing the same variable. Enforcing this rule is called the occurs check.
To avoid circular substitutions, variables are renamed when necessary. This process is called standardizing apart.

See the book by Russell and Norvig for an actual step-by-step unification algorithm.

The substitution that unifies two terms can have size exponential in the size of the input terms. For example, consider unifying A = P( f(a,a) g(u,u) h(v,v) i(w,w) )and B = P(u,v,w,x). The unifying substitution is

{ u := f(a,a)
v := g(f(a,a),f(a,a))
w := h( g(f(a,a),f(a,a)), g(f(a,a),f(a,a)) )
x := ... }

What this example shows is that the usual notation for writing down terms should be avoided. Good data structures for implementing unification and resolution are beyond the scope of this course.

CONTROL STRATEGIES FOR RESOLUTION

When doing a resolution proof, typically at each step there are many pairs of parent clauses that could be resolved. A control strategy is a policy for prioritizing which resolutions to perform next. Most strategies have the form "At least one parent of each resolution step must satisfy the syntactic property ...."

Definition: A control strategy is complete if its use preserves refutation-completeness, i.e. if a contradiction exists, it can be found while respecting the strategy.

If a policy allows only a finite number of possible resolutions, then theorem-proving always terminates in bounded time In this case completeness must fail because it would contradict the fact that FOL is only semi-decidable, and not decidable.

Any policy that places a fixed upper bound on the length of the clauses that may be used in a proof only allows a finite number of resolutions, hence is incomplete.

INCOMPLETE STRATEGIES

Let's look first at two strategies that are not complete, but are still used often for efficiency.

Unit resolution is the policy that at least one parent of each resolution step must be a unit clause, i.e. a single literal. Unit resolution is what we called unit propagation when discussing the DPLL algorithm for propositional satisfiability.

Under unit resolution the conclusion of each resolution step is shorter than its non-unit parent, so unit resolution must be incomplete. For example, it fails to derive false from these four clauses:

{ P v Q ~P v Q P v ~Q ~P v ~Q }

Input resolution is the policy that at least one parent of each resolution step must be in the original knowledge base, or part of the negated goal. The eats(jo,fish) proof from February 26 is an example of input resolution.

This strategy is not complete either, but it can be efficient. It fails on the same example as unit resolution. (Just assume that any one of the four clauses is the negated goal.)

Both unit resolution and input resolution are complete when all clauses are Horn clauses. A Horn clause is a clause with at most one positive literal.

Unit preference is the heuristic of prioritizing resolutions where one parent is a unit clause. This heuristic does not actually eliminate any resolutions. It can be used in combination with other strategies that do, without changing their completeness or incompleteness