- Asked 2/12
- 2072 Asoj · 7 marks
- 2074 Bhadra · 8 marks
Resolution: John likes peanuts
Short answer
Convert facts to clauses, add negated goal ¬Likes(John, Peanuts). Resolve with C1 to ¬Food(Peanuts), with C4 to Killed(Bill), with C8 to ¬Alive(Bill), with C6 to empty clause. Thus John likes peanuts.
Assume the following facts: 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. Prove that John likes peanuts using resolution refutation.
Step 1: Statements in FOPL
Predicates: Food(x), Likes(x,y), Eats(x,y), Killed(x), Alive(x).
- ∀x Food(x) → Likes(John, x)
- Food(Apple)
- Food(Chicken)
- ∀x ∀y [Eats(x,y) ∧ ¬Killed(x)] → Food(y)
- Eats(Bill, Peanuts) ∧ Alive(Bill)
- ∀x Eats(Bill, x) → Eats(Sue, x)
- ∀x Alive(x) → ¬Killed(x) (common-sense axiom: someone alive is not killed)
Goal: Likes(John, Peanuts)
Step 2: Clause form
| No. | Clause |
|---|---|
| C1 | ¬Food(x) ∨ Likes(John, x) |
| C2 | Food(Apple) |
| C3 | Food(Chicken) |
| C4 | ¬Eats(x,y) ∨ Killed(x) ∨ Food(y) |
| C5 | Eats(Bill, Peanuts) |
| C6 | Alive(Bill) |
| C7 | ¬Eats(Bill, x) ∨ Eats(Sue, x) |
| C8 | ¬Alive(x) ∨ ¬Killed(x) |
Step 3: Negated goal
C9: ¬Likes(John, Peanuts)
Step 4: Resolution refutation
| Step | Resolve | Substitution | Resolvent |
|---|---|---|---|
| 1 | C9 and C1 | x/Peanuts | R1: ¬Food(Peanuts) |
| 2 | R1 and C4 | y/Peanuts | R2: ¬Eats(x, Peanuts) ∨ Killed(x) |
| 3 | R2 and C5 | x/Bill | R3: Killed(Bill) |
| 4 | R3 and C8 | x/Bill | R4: ¬Alive(Bill) |
| 5 | R4 and C6 | R5: empty clause (□) |
¬Likes(John,Peanuts) + C1 -> ¬Food(Peanuts)
+ C4 -> ¬Eats(x,Peanuts) ∨ Killed(x)
+ C5 -> Killed(Bill)
+ C8 -> ¬Alive(Bill)
+ C6 -> □
The empty clause is derived, so the assumption ¬Likes(John, Peanuts) is false. Hence John likes peanuts. (Clauses C2, C3 and C7 are not needed in the proof.)
✓ Answer checked by Claude Opus 5.5 (high effort)
Related questions
- Resolution: Mary loves John · Artificial Intelligence, chapter 4
- Resolution: horse, Bluebeard, Charlie · Artificial Intelligence, chapter 4
- Resolution: American sells weapons · Artificial Intelligence, chapter 4 · asked 2×