"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