Next: About this document ...
An example of resolution in predicate calculus
Represent the following set of axioms in predicate calculus and
convert each formula to clause form. Prove that the goal can be
derived from the axioms via resolution.
 All dogs howl at night
 Anyone who has any cats will not have any mice
 Light sleepers do not have anything which howls at night
 John has either a cat or a dog.
 Goal: If John is a light sleeper, then John does not have any mice.
First we write the axioms in predicate calculus:


or the equivalent expression


 Goal:
which, when negated, becomes
We convert to CNF:
 eliminate implications and drop universal quantifiers
1.
 eliminate implications
Move negations
Move universal quantifiers, drop them, and rename variables
2.
 eliminate implications
Move negations:
Move universal quantifiers, drop them, and rename variables
3.
 eliminate existential quantifier. This introduces a Skolem constant
(since there is no universal quantifier).
Eliminate conjunctions
4a.
4b.
 eliminate implications
move negations
Eliminate existential quantifier. This introduces a Skolem constant (since
there is no universal quantifier)
eliminate conjunctions
5a.
5b.
5c.
So, in conclusion, we have the following clauses:
1.
2.
3.
4a.
4b.
5a.
5b.
5c.
We now use resolution to find a condraddiction:
 resolve 3.
with 5a.
unfying {w/John} to obtain 9.
 resolve 9.
with 1.
unifying {x/r} to obtain 10.
 resolve 10.
with 4b.
unifying {r/S} to obtain 11.
 resolve 11.
with 4s.
to obtain 12.
 resolve 12. with
2.
unifying {y/S} to obtain 13.
 resolve 13.
with 4a.
unifying {p/John} to obtain 14.
 resolve 14.
with
5b.
unifying {z/M} to obtain 15.
 resolve 15. with 5c. to obtain a contradiction.
Next: About this document ...
Maria Gini
20041117