Search code examples
artificial-intelligencepredicatetheorem-proving

Theorem Solution by Resolution Refutation

I have the following problem which I need to solve by resolution method in Artificial Intelligence

enter image description here

I don't understand why the negation of dog(x) is added in the first clause and ///y in the fourth clause why negation of animal(Y) is added ...

I mean what is the need of negation there?

Solution

  • Recall that logical implication P → Q is equivalent to ¬P ∨ Q. You can verify this by looking at the truth table:

       P Q  P → Q
   0 0    1
   1 0    0
   0 1    1
   1 1    1

    Now clearly dog(X) → animal(X) is equivalent to ¬dog(X) ∨ animal(X) which is a disjunction of literals therefore is a clause.

    The same reasoning applies to animal(Y) → die(Y).

    As soon as you have got a set of formulas in clausal form that is equivalent to your input knowledge base, you can apply binary resolution to check if your knowledge base is consistent, or to prove a goal.

    To prove a goal you add a negation of it to your consistent knowledge base and see if the knowledge base with the added negation of the goal becomes inconsistent.