---
title: "Resolution: John likes peanuts"
subject: "Artificial Intelligence"
chapter: 4
key: "semester_6/artificial_intelligence:resolution-john-likes-peanuts"
source: https://www.bctengineer.com/q/semester_6/artificial_intelligence/resolution-john-likes-peanuts
site: BCT Engineering
---

# Resolution: John likes peanuts

Artificial Intelligence · Chapter 4: Knowledge Representation, Inference & Reasoning

- Asked in: 2072 Asoj, 7 marks; 2074 Bhadra, 8 marks (asked 2 times)
- Video: [Resolution in Predicate logic || Is John like peanuts || Artificial Intelligence](https://www.youtube.com/watch?v=zmhfHsOLO6w) — Sudhakar Atchala
- Answer checked by Claude Opus 5.5 (high effort) on 2026-10-14
- Page: https://www.bctengineer.com/q/semester_6/artificial_intelligence/resolution-john-likes-peanuts
- Whole chapter: https://www.bctengineer.com/md/semester_6/artificial_intelligence/chapter-4

## Question

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.

## 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.

## Answer

#### Step 1: Statements in FOPL
Predicates: Food(x), Likes(x,y), Eats(x,y), Killed(x), Alive(x).

1. ∀x Food(x) → Likes(John, x)
2. Food(Apple)
3. Food(Chicken)
4. ∀x ∀y [Eats(x,y) ∧ ¬Killed(x)] → Food(y)
5. Eats(Bill, Peanuts) ∧ Alive(Bill)
6. ∀x Eats(Bill, x) → Eats(Sue, x)
7. ∀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 (□)** |

```text
¬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.)

## Check yourself

The answer's key points as multiple-choice questions, with the correct option and why.

1. What is the clause form of 'Anything anyone eats and isn't killed by is food'?
   A. ¬Eats(x,y) ∨ Killed(x) ∨ Food(y)
   B. Eats(x,y) ∨ Killed(x) ∨ Food(y)
   C. ¬Eats(x,y) ∨ ¬Killed(x) ∨ ¬Food(y)
   D. Food(y) → Eats(x,y)
   Answer: A. (Eats ∧ ¬Killed) → Food becomes ¬Eats ∨ Killed ∨ Food. (Key point: Clause form of rule 4)

2. Which common-sense axiom is added to link 'alive' with 'not killed'?
   A. ∀x Alive(x) → ¬Killed(x)
   B. ∀x Killed(x) → Alive(x)
   C. ∀x Food(x) → Alive(x)
   D. Alive(John)
   Answer: A. Clause ¬Alive(x) ∨ ¬Killed(x) is needed to use the fact Alive(Bill). (Key point: Extra axiom)

3. Which clause is added as the negated goal?
   A. Likes(John, Peanuts)
   B. ¬Likes(John, Peanuts)
   C. ¬Food(Peanuts)
   D. Eats(Bill, Peanuts)
   Answer: B. We assume John does not like peanuts and look for a contradiction. (Key point: Negated goal)

4. How does the proof reach the empty clause?
   A. ¬Likes → ¬Food(Peanuts) → (C4, C5) Killed(Bill) → (C8) ¬Alive(Bill) → (C6) empty
   B. ¬Likes → Food(Apple) → empty
   C. ¬Likes → Eats(Sue, Peanuts) → empty
   D. ¬Likes → Killed(John) → empty
   Answer: A. Resolving with C1, C4, C5, C8 and C6 gives the contradiction; C2, C3, C7 are not needed. (Key point: Proof chain)

## Related in Artificial Intelligence

- [Resolution: Mary loves John](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Aresolution-mary-john-football) — Artificial Intelligence, chapter 4
- [Resolution: horse, Bluebeard, Charlie](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Aresolution-horses-charlie) — Artificial Intelligence, chapter 4
- [Resolution: American sells weapons](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Aresolution-american-criminal) — Artificial Intelligence, chapter 4, asked 2×