CODEWITHSUNDEEP
artificial-intelligencepredicatetheorem-proving
techno
techno

Reputation: 6500

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?

Upvotes: 0

Views: 147

Answers (1)

Dima Chubarov
Dima Chubarov

Reputation: 17169

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.

Upvotes: 1

Related Questions