   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.

1. All dogs howl at night
2. Anyone who has any cats will not have any mice
3. Light sleepers do not have anything which howls at night
4. John has either a cat or a dog.
5. Goal: If John is a light sleeper, then John does not have any mice.

First we write the axioms in predicate calculus:

1. 2. or the equivalent expression 3. 4. 5. Goal: which, when negated, becomes We convert to CNF:

1. eliminate implications and drop universal quantifiers

1. 2. eliminate implications Move negations  Move universal quantifiers, drop them, and rename variables

2. 3. eliminate implications Move negations: Move universal quantifiers, drop them, and rename variables

3. 4. eliminate existential quantifier. This introduces a Skolem constant (since there is no universal quantifier). Eliminate conjunctions

4a. 4b. 5. 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.   