CSE 473 Autumn 1998, Copyright, S. Tanimoto, Univ. of Washington 
Introduction to Artificial Intelligence (Nov 30, 1998)

"Reasoning with Resolution"

Motivation: Using Logic to Make Sound Inferences:
 

1. Inference: Deriving new statements from old.

2. Sound inferences: those whose negations would be inconsistent with their premises.

3. Logic offers both languages for representing the knowledge and means for making sound inferences.
 
 
 
 
 

Resolution in the Propositional Calculus

1. Consider Modus Ponens:  P,   P -> Q  imply Q
This can be rewritten  P, ~P V Q   imply  Q.
This is an example of "resolution"

2. Literal:  An atomic proposition, with or without a negation sign in front of it.
Examples:  P, ~P, Q, ~Q.

3. Clause:  a disjunction of  literals.
Examples:  P V Q,  ~P V R,  P,  ~P,  P V ~P,  P V Q V R.
There is a special clause called the null clause which contains 0 literals.

4. A pair of clauses is resolvable if they contain a complementary pair of literals.

5. Example of a resolvable pair of clauses:  P1 V Q V R,  P2 V ~Q.  Here Q and ~Q are the complementary literals.

6. A resolvent of a resolvable pair of clauses is obtained by disjoining the two clauses and deleting a pair of complementary literals.
For the above example, there is a unique resolvent (up to reordering of the literals):
P1 V R V P2.
 
 
 

Examples of Resolution with the Predicate Calculus
 
 
 

1.  P(a) V ~Q(b),  R(x) V Q(b).  This pair is resolvable because ~Q(b) and Q(b) are complementary literals.  The resolvent is P(a) V R(x).

2.  ~P(x), P(a) V Q(b)  are not immediately resolvable.  However, note that there is a variable x in one of the literals of a potentially complementary pair of literals.  If a substitution is made (for this variable x) of the term a, then we have the resulting pair of clauses:
~P(a), P(a) V Q(b).
These clauses are resolvable and have the resolvent Q(b).

3. The unit clauses P(a) and ~P(a) form a complementary literal pair, and they have the null clause as their resolvent.  The null clause represents a contradiction.

4. P(x, y) V Q(x)  and ~Q(f(a))  have a resolvent   P(f(a), y). To get it, we first have to make the substituion of f(a) for x in the first clause.  Then we proceed to list (with OR signs if more than one) the literals that remain after the complementary pair has been marked out.
 
 
 

Unification
 
 

The process of finding a set of substitutions (of terms for variables) that make two (or more) literals match exactly is called unification.

The resulting substitution (set) is called a unifier.

1.  Given Q(x, y) and Q(a, b),  there is a unifier { a/x, b/y }.  This means substitute a for x and by for y.

2.  Given   P(x),   P(y),  these could be unified by the subtitution of a/x and a/y.   But we could avoid turing the argument into a constant by making the substitution of y/x in the second literal.
The unifier { y/x } is said to be more general than the unifier {a/x, a/y }.

A unifier for a particular set of literals is a most general unifier for that set if there is no other unifier for that set that is more general.

When substituting a term for a variable, the term must not contain any instance of the same variable.  If such a subtitution appears necessary to amke a unifier, then the literals being matched are not unifiable.

For example,   P(x, f(x))  and P(x, x) are not unifiable, because we are not allowed to make the substitution of f(x) for x.

When a unfier exists for a set of literals, it is possible to find a most general unifier by scanning each literal from left to right in parallel, stopping the scan at each symbol where there is a mismatch.  Whenever a mismatch is reached, it must be resolved by making a substitution of a term for a variable.  This substitution is immediately applied to all occurrences of the variable in the literals
and all occurrences of the variable in the terms of unifier as thus far constructed.
Then the scan continues.
 
 
 
 
 
 
 

Clause Form

Resolution is a process performed on clauses.  Therefore, in order to use resolution, one's premises must be represented as a set of clauses.

Resolution can be used to show that an inconsistent set of formulas actually is inconsistent.  This is very important, as it means that resolution can be used as a means to prove theorems.  We'll also see how it can be used to solve problems.

The idea of demonstrating inconsistency of a set of formulas is the following:
1. represent the formulas as a set of clauses.
2. apply resolution to the clauses repeatedly until the null clause is derived.
3. When the null clause is derived, that is an indication that the original set of clauses was inconsistent.  In other words, they imply a contradiction.

To convert a formula to clauses, a series of steps must be taken...

1. eliminate implication signs using the identity  P -> Q  iff ~P V Q.
2. minimize the scopes of the negation signs, using the following identities...
~(P V Q) iff ~P ^ ~Q.
~(P ^ Q)  iff  ~P V ~Q.
~(exists x) P(x)   iff (forall x) ~P(x)
~(forall x) P(x)  iff  (exists x) ~P(x)
3. eliminate double negations using the identity ~~P iff P.
4. standardize the variables of the formula by using a unique variable for each quantifier.
5. eliminate the existential quantifiers using the Skolemization method.
6. eliminate universal quantifiers.
7. convert to conjunctive normal form.
8. break up into clauses -- each conjunct becomes one clause.
 
 
 

Answer Extraction

Problem solving method...
1. Express premises in predicate logic.
2. Express question in predicate logic as an assertion that the answer exists.
3. Negate the assertion that an answer exists and make this negation an extra premise.
4. Put all premises in clause form.
5. Apply resolution to find the null clause, keeping track of all substitutions performed and resolution steps made.
6. Reapply the same substitutions to the same clauses, except that you should replace the special premise by a tautology consisting of it OR'd with its negation.
7. When you arrive at the resolution step where originally you derived the null clause, you should derive now a unit clause that expresses the answer to the original problem.

See the example in the textbook and this additional one.
 
 


 
 

Last modified: November 30, 1998

Steve Tanimoto

tanimoto@cs.washington.edu