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. $\forall x Dog(x) \Rightarrow Howls(x)$
2. $\forall \,x \forall \,y \:Has(x,y) \land Cat(y) \Rightarrow \neg [\exists \,z Has(x,z) \land Mice(z)]$
   or the equivalent expression $\forall x \forall y \forall z \:Has(x,y) \land Cat(y) \land Mice(z) \Rightarrow \neg Has(x,z)$
3. $\forall \,x \:Lightsleep(x) \Rightarrow \neg [\exists \,y \: Has(x,y) and Howls(y)]$
4. $\exists y \:Has(John,y) \land [Cat(y) \lor Dog(y)]$
5. Goal: $Lightsleep(John) \Rightarrow \neg [\exists \,y Has(John,y) \land Mice(y)]$
   which, when negated, becomes
   $\neg [Lightsleep(John) \Rightarrow \neg [\exists \,y \:Has(John,y) \land Mice(y)]]$

We convert to CNF:

1. eliminate implications and drop universal quantifiers

   1. $\neg Dog(x) \lor Howls(x)$
   

2. eliminate implications

   $\forall \,x \forall \,y \: \neg[Has(x,y) \land Cat(y)] \lor \neg [\exists \,z \:Has(x,z) \land Mice(z)]$

   Move negations

   $\forall x \forall y \:\neg Has(x,y) \lor \neg Cat(y) \lor \forall z \: \neg[Has(x,z) \land Mice(z)]$

   $\forall x \forall y \: \neg Has(x,y) \lor \neg Cat(y) \lor \forall z \:[\neg Has(x,z) \lor \neg Mice(z)]$

   Move universal quantifiers, drop them, and rename variables

   2. $\neg Has(x,y) \lor \neg Cat(y) \lor \neg Has(x,z) \lor \neg Mice(z)$

3. eliminate implications

   $\forall \,x \: \neg Lightsleep(x) \lor \neg [\exists \,y \: Has(x,y) \land Howls(y)]$

   Move negations:

   $\forall x \: \neg Lightsleep(x) \lor \forall y \:[\neg Has(x,y) \lor \neg Howls(y)]$

   Move universal quantifiers, drop them, and rename variables

   3. $\neg Lightsleep(w) \lor \neg Has(w,r) \lor \neg Howls(r)$

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

   $Has(John,S) \land [Cat(S) \lor Dog(S)]$

   Eliminate conjunctions

   4a. $Has(John,S)$

   4b. $Cat(S) \lor Dog(S)$

5. eliminate implications

   $\neg [\neg Lightsleep(John) \lor \neg [\exists \, y \:[Has(John,y) \land Mice(y)]]$

   move negations

   $Lightsleep(John) \land \exists \,y \:Has(John,y) \land Mice(y)$

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

   $Lightsleep(John) \land Has(John,M) \land Mice(M)$

   eliminate conjunctions

   5a. $Lightsleep(John)$
   5b. $Has(John,M)$
   5c. $Mice(M)$

So, in conclusion, we have the following clauses:

1. $\neg Dog(x) \lor Howls(x)$
2. $\neg Has(p,y) \lor \neg Cat(y) \lor \neg Has(p,z) \lor \neg Mice(z)$
3. $\neg Lightsleep(w) \lor \neg Has(w,r) \lor \neg Howls(r)$
4a. $Has(John,S)$
4b. $Cat(S) \lor Dog(S)$
5a. $Lightsleep(John)$
5b. $Has(John,M)$
5c. $Mice(M)$

We now use resolution to find a condraddiction:

• resolve 3. $\neg Lightsleep(w) \lor \neg Has(w,r) \lor \neg Howls(r)$ with 5a. $Lightsleep(John)$
  unfying {w/John} to obtain 9. $\neg Has(John,r) \lor \neg Howls(r)$
• resolve 9. $\neg Has(John,r) \lor \neg Howls(r)$ with 1. $\neg Dog(x) \lor Howls(x)$
  unifying {x/r} to obtain 10. $\neg Has(John,r) \lor \neg Dog(r)$
• resolve 10. $\neg Has(John,r) \lor \neg Dog(r)$ with 4b. $Cat(S) \lor Dog(S)$
  unifying {r/S} to obtain 11. $\neg Has(John,S) \lor Cat(S)$
• resolve 11. $\neg Has(John,S) \lor Cat(S)$ with 4s. $Has(John,S)$ to obtain 12. $Cat(S)$
• resolve 12. $Cat(S)$ with 2. $\neg Has(p,y) \lor \neg Cat(y) \lor \neg Has(p,z) \lor \neg Mice(z)$
  unifying {y/S} to obtain 13. $\neg Has(p,S) \lor \neg Has(p,z) \lor \neg Mice(z)$
• resolve 13. $\neg Has(p,S) \lor \neg Has(p,z) \lor \neg Mice(z)$ with 4a. $Has(John,S)$
  unifying {p/John} to obtain 14. $\neg Has(John,z) \lor \neg Mice(z)$
• resolve 14. $\neg Has(John,z) \lor \neg Mice(z)$ with 5b. $Has(John,M)$
  unifying {z/M} to obtain 15. $\neg Mice(M)$
• resolve 15. $\neg Mice(M)$ with 5c. $Mice(M)$ to obtain a contradiction.