---
title: "Resolution: horse, Bluebeard, Charlie"
subject: "Artificial Intelligence"
chapter: 4
key: "semester_6/artificial_intelligence:resolution-horses-charlie"
source: https://www.bctengineer.com/q/semester_6/artificial_intelligence/resolution-horses-charlie
site: BCT Engineering
---

# Resolution: horse, Bluebeard, Charlie

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

- Asked in: 2073 Bhadra, 8 marks
- Answer checked by Claude Opus 5.5 (high effort) on 2026-10-14
- Page: https://www.bctengineer.com/q/semester_6/artificial_intelligence/resolution-horses-charlie
- Whole chapter: https://www.bctengineer.com/md/semester_6/artificial_intelligence/chapter-4

## Question

Assume the following facts: i) Horses, cows, pigs are mammals. ii) An offspring of a horse is a horse. iii) Bluebeard is a horse. iv) Bluebeard is Charlie's parent. v) Offspring and parent are inverse relations. vi) Every mammal has a parent. Prove Charlie is a horse using resolution refutation.

## Short answer

Clauses from facts include Horse(Bluebeard) and Parent(Bluebeard,Charlie). Adding ¬Horse(Charlie) and resolving with offspring and parent links yields ¬Horse(Bluebeard), contradicting the fact. Empty clause proves Charlie is a horse.

## Answer

#### Step 1: Statements in FOPL
Predicates: Horse(x), Cow(x), Pig(x), Mammal(x), Parent(x, y) = x is a parent of y, Offspring(y, x) = y is an offspring of x.

1. ∀x [Horse(x) ∨ Cow(x) ∨ Pig(x)] → Mammal(x)
2. ∀x ∀y [Horse(x) ∧ Offspring(y, x)] → Horse(y)
3. Horse(Bluebeard)
4. Parent(Bluebeard, Charlie)
5. ∀x ∀y Parent(x, y) ↔ Offspring(y, x)
6. ∀x Mammal(x) → ∃y Parent(y, x)

**Goal:** Horse(Charlie)

#### Step 2: Clauses
| No. | Clause |
|---|---|
| C1 | ¬Horse(x) ∨ Mammal(x) (and similarly for Cow, Pig) |
| C2 | ¬Horse(x) ∨ ¬Offspring(y, x) ∨ Horse(y) |
| C3 | Horse(Bluebeard) |
| C4 | Parent(Bluebeard, Charlie) |
| C5a | ¬Parent(x, y) ∨ Offspring(y, x) |
| C5b | ¬Offspring(y, x) ∨ Parent(x, y) |
| C6 | ¬Mammal(x) ∨ Parent(g(x), x) (g is a Skolem function) |

#### Step 3: Negated goal
C7: **¬Horse(Charlie)**

#### Step 4: Resolution
| Step | Resolve | Substitution | Resolvent |
|---|---|---|---|
| 1 | C7 and C2 | y/Charlie | R1: ¬Horse(x) ∨ ¬Offspring(Charlie, x) |
| 2 | R1 and C5a | y/Charlie | R2: ¬Horse(x) ∨ ¬Parent(x, Charlie) |
| 3 | R2 and C4 | x/Bluebeard | R3: ¬Horse(Bluebeard) |
| 4 | R3 and C3 | | **R4: empty clause (□)** |

```text
¬Horse(Charlie) + C2 -> ¬Horse(x) ∨ ¬Offspring(Charlie,x)
   + C5a -> ¬Horse(x) ∨ ¬Parent(x,Charlie)
   + C4 {x/Bluebeard} -> ¬Horse(Bluebeard)
   + C3 -> □
```
The empty clause is derived. **Hence Charlie is a horse.** (C1, C5b and C6 are not needed in this proof.)

## Check yourself

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

1. Which clause lets Parent(Bluebeard, Charlie) be used to get Offspring(Charlie, Bluebeard)?
   A. ¬Offspring(y,x) ∨ Parent(y,x)
   B. ¬Parent(x,y) ∨ Offspring(y,x)
   C. Parent(x,y) ∨ Offspring(x,y)
   D. ¬Parent(x,y) ∨ ¬Offspring(y,x)
   Answer: B. Offspring and parent are inverse: Parent(x,y) implies Offspring(y,x). (Key point: Inverse relation clause)

2. Which clauses are actually needed in the refutation?
   A. Negated goal, offspring-of-horse rule, inverse rule, Parent fact and Horse(Bluebeard)
   B. All clauses including the mammal and Skolem clauses
   C. Only the mammal clause and Horse(Bluebeard)
   D. Only the Skolem clause for every mammal has a parent
   Answer: A. The mammal clause C1, converse C5b and Skolem C6 are not needed. (Key point: Proof path)

3. In step 2, resolving ¬Horse(x) ∨ ¬Parent(x,Charlie) with Parent(Bluebeard,Charlie) needs which substitution?
   A. x/Charlie
   B. y/Bluebeard
   C. x/Bluebeard
   D. x/Horse
   Answer: C. Unifying Parent(x,Charlie) with Parent(Bluebeard,Charlie) gives x = Bluebeard. (Key point: Substitution)

## Related in Artificial Intelligence

- [Resolution: John likes peanuts](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Aresolution-john-likes-peanuts) — Artificial Intelligence, chapter 4, asked 2×
- [Resolution: Mary loves John](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Aresolution-mary-john-football) — 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×
- [Frames, semantic net; sakti gauchan](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Aframes-semantic-net-convert-sentences) — Artificial Intelligence, chapter 5

## Related in other subjects

- [Every RE has NFA; ε-NFA for bb(a∪b)*ab](https://www.bctengineer.com/question.md?key=semester_3%2Ftheory_of_computation%3Are-to-nfa-bb-aub-ab) — Theory of Computation, chapter 2
- [Prove mean annual flood has 2.33-year return period](https://www.bctengineer.com/question.md?key=semester_5%2Fengineering_hydrology%3Agumbel-mean-flood-2-33yr) — Engineering Hydrology, chapter 6
- [Absolute vs relative dispersion; horses](https://www.bctengineer.com/question.md?key=semester_5%2Fprobability_and_statistics%3Ahorses-consistency-dispersion) — Probability and Statistics, chapter 1
- [Log-antilog circuit: Vo in terms of Vi and VR](https://www.bctengineer.com/question.md?key=semester_4%2Fadvanced_electronics%3Alog-antilog-circuit-vo-vi) — Advanced Electronics, chapter 5, asked 3×