Artificial Intelligence
(CSE3002)
Resolution
Resolution in FOL
• Resolution is a theorem proving technique that proceeds by building proofs by contradictions. (Proof
of refutation)
• Resolution is used, if there are various statements are given, and we need to prove a conclusion of
those statements.
• Unification is a key concept in proofs by resolutions.
• Resolution is a single inference rule which can efficiently operate on the conjunctive normal form or
clausal form.
• Clause: Disjunction of literals (an atomic sentence) is called a clause. It is also known as a unit clause.
• Conjunctive Normal Form: A sentence represented as a conjunction of clauses is said to
be conjunctive normal form or CNF.
Steps for Resolution:
1.Conversion of facts into First-Order Logic.
2.Convert FOL statements into CNF (conjunctive normal form).
3.Negate the statement which needs to prove (proof by contradiction).
4.Draw resolution graph (unification).
Remember the following
5.￢ A and A , Cancelled each other
6. A →B is ¬ A V B
Example 1 :
1. If it is sunny and warm day you will enjoy.
2. If it is raining you will get wet.
3. It is warm day.
4. It is raining.
5. It is sunny.
• Goal: You will enjoy
• Prove: Enjoy
Step 1: Conversion of facts to First Order Logic:
• If It is sunny and warm day you will enjoy.
Sunny Ʌ warm ⇒ enjoy
• If it is raining you will get wet.
Raining ⇒ wet
• It is warm day
Warm
• It is raining
Raining
• It is sunny
Sunny
Step 2: Conversion to CNF (Conjunctive Normal Form ) :
• Sunny Ʌ Warm ⇒ enjoy
Eliminate implication:
¬(Sunny Ʌ warm) V enjoy Rule: A →B is ¬ A V B
Moving negation inside
¬ Sunny V ¬ warm V enjoy
• Raining ⇒ wet
Eliminate implication:
¬ raining V wet
• Warm
• Raining
• Sunny
Step 3 & 4:Resolution graph
• Negate the statements to be proved: ¬enjoy
• Now take the statements one by one and create resolution graph.
Example 2
• Consider the following Knowledge Base:
1. The humidity is high or the sky is cloudy.
2. If the sky is cloudy, then it will rain.
3. If the humidity is high, then it is hot.
4. It is not hot.
• Goal: It will rain
Conversion facts to First Order Logic
1. The humidity is high or the sky is cloudy.
2. If the sky is cloudy, then it will rain.
3. If the humidity is high, then it is hot.
4. It is not hot.
Let P: The humidity is high.
Let Q : Sky is cloudy
The humidity is high or the sky is cloudy
PVQ
Conversion to first order logic
1. The humidity is high or the sky is cloudy.
2. If the sky is cloudy, then it will rain.
3. If the humidity is high, then it is hot.
4. It is not hot.
Goal: It will rain
Let Q: Sky is cloudy
Let R : It will rain
If the sky is cloudy, then it will rain
Q⇒R
Conversion to first order logic
1. The humidity is high or the sky is cloudy.
2. If the sky is cloudy, then it will rain.
3. If the humidity is high, then it is hot.
4. It is not hot.
Goal: It will rain
Let P: The humidity is high
Let S : It is hot
If the humidity is high, then it is hot.
P⇒S
Conversion to first order logic
1. The humidity is high or the sky is cloudy.
2. If the sky is cloudy, then it will rain.
3. If the humidity is high, then it is hot.
4. It is not hot.
Goal: It will rain
Let S : It is hot
It is not hot
¬S
Conversion it to CNF
Negation of Goal (¬R): It will not rain
Resolution graph
Exercise
1.John likes all kind of food.
2.Apple and vegetable are food
3.Anything anyone eats and not killed is food.
4.Anil eats peanuts and still alive
5.Harry eats everything that Anil eats.
Prove by resolution that:
John likes peanuts.
Step-2: Conversion of FOL into CNF
In First order logic resolution, it is required to convert the FOL into CNF as CNF form makes easier for
resolution proofs.
Step-4: Draw Resolution graph:
Now in this step, we will solve the problem by resolution tree using substitution.
For the above problem, it will be given as follows
Exercise:
Consider the following KB:
• John likes all kinds of food.
• Apples are food.
• Chicken is food.
• Anything anyone eats and isn’t killed by is food.
• Bill eats peanuts and is still alive.
• Sue eats everything Bill eats.
i. Translate these sentences into formulas in
FOPC(First order predicate calculus) or FOL.
ii. Convert the formulas into clause form.
iii. Use resolution to prove that John likes
peanuts and draw the graph
iv. Use resolution to answer the question, “What
food does Sue eat?”
(a) Translate these sentences into formulas in FOPC.
1. ∀x F ood(x) → Likes(John, x)
2. F ood(Apples)
3. F ood(Chicken)
4. ∀x∃y Eats(y, x) ∧ ¬KilledBy(y, x) → F ood(x)
5. Eats(Bill, P eanuts) ∧ ¬KilledBy(Bill, P eanuts)
6. ∀x Eats(Bill, x) → Eats(Sue, x)
(b) Convert the formulas of part (a) into clause form.
1. ¬F ood(x) ∨ Likes(John, x)
2. F ood(Apples)
3. F ood(Chicken)
4. ¬Eats(y, x) ∨ KilledBy(y, x) ∨ F ood(x)
5. Eats(Bill, P eanuts)
6. ¬KilledBy(Bill, P eanuts)
7. ¬Eats(Bill, x) ∨ Eats(Sue, x)
(c) Use resolution to prove that John likes peanuts.
8. ¬Likes(John, P eanuts) negated conclusion
9. ¬F ood(P eanuts) 1 and 8
10. ¬Eats(y, P eanuts) ∨ KilledBy(y, P eanuts) 4 and 9
11. KilledBy(Bill, P eanuts) 5 and 10
12. ⊥ 6 and 11
(d) Use resolution to answer the question, “What food does Sue eat?”
13. ¬Eats(Sue, x) negated query
14. ¬Eats(Bill, x) 7 and 13
15. ⊥ 5 and 14, unifying Peanuts/x
