next up previous
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.

  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:




next up previous
Next: About this document ...
Maria Gini 2004-11-17