- 2073 Bhadra · 8 marks
Resolution: horse, Bluebeard, Charlie
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.
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.
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.
- ∀x [Horse(x) ∨ Cow(x) ∨ Pig(x)] → Mammal(x)
- ∀x ∀y [Horse(x) ∧ Offspring(y, x)] → Horse(y)
- Horse(Bluebeard)
- Parent(Bluebeard, Charlie)
- ∀x ∀y Parent(x, y) ↔ Offspring(y, x)
- ∀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 (□) |
¬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.)
✓ Answer checked by Claude Opus 5.5 (high effort)
Related questions
- Resolution: John likes peanuts · Artificial Intelligence, chapter 4 · asked 2×
- Resolution: Mary loves John · Artificial Intelligence, chapter 4
- Resolution: American sells weapons · Artificial Intelligence, chapter 4 · asked 2×
- Frames, semantic net; sakti gauchan · Artificial Intelligence, chapter 5
- Every RE has NFA; ε-NFA for bb(a∪b)*ab · Theory of Computation, chapter 2
- Prove mean annual flood has 2.33-year return period · Engineering Hydrology, chapter 6
- Absolute vs relative dispersion; horses · Probability and Statistics, chapter 1
- Log-antilog circuit: Vo in terms of Vi and VR · Advanced Electronics, chapter 5 · asked 3×