- Asked 2/12
- 2069 Bhadra · 10 marks
- 2075 Baisakh · 8 marks
Resolution: American sells weapons
Short answer
Convert premises to clauses, add negation of goal ¬Criminal(John). Resolve repeatedly: ¬Criminal(John) with C1 gives ¬American(John)∨...; after successive resolutions, empty clause is derived. Therefore, John is a criminal.
Given premises: Every American who sells weapons to hostile nations is a criminal. The country Abc is an enemy of America. All of the missiles in Abc were sold by John. John is an American. Prove that John is a criminal using FOPL based resolution refutation.
Step 1: Statements in FOPL
Predicates: American(x), Weapon(x), Missile(x), Sells(x,y,z) = x sells y to z, Hostile(x), Enemy(x,y), Criminal(x), In(x,y) = x is located in y.
- ∀x ∀y ∀z [American(x) ∧ Weapon(y) ∧ Sells(x,y,z) ∧ Hostile(z)] → Criminal(x)
- Enemy(Abc, America)
- ∀x [Missile(x) ∧ In(x, Abc)] → Sells(John, x, Abc)
- American(John)
Background assumptions (common-sense facts needed): 5. Abc has a missile M1: Missile(M1), In(M1, Abc) 6. ∀x Missile(x) → Weapon(x) 7. ∀x Enemy(x, America) → Hostile(x)
Goal: Criminal(John).
Step 2: Convert to clauses (CNF)
| No. | Clause |
|---|---|
| C1 | ¬American(x) ∨ ¬Weapon(y) ∨ ¬Sells(x,y,z) ∨ ¬Hostile(z) ∨ Criminal(x) |
| C2 | Enemy(Abc, America) |
| C3 | ¬Missile(x) ∨ ¬In(x,Abc) ∨ Sells(John,x,Abc) |
| C4 | American(John) |
| C5 | Missile(M1) |
| C6 | In(M1, Abc) |
| C7 | ¬Missile(x) ∨ Weapon(x) |
| C8 | ¬Enemy(x, America) ∨ Hostile(x) |
Step 3: Negate the goal
C9: ¬Criminal(John)
Step 4: Resolution refutation
| Step | Resolve | Substitution | Resolvent |
|---|---|---|---|
| 1 | C9 and C1 | x/John | R1: ¬American(John) ∨ ¬Weapon(y) ∨ ¬Sells(John,y,z) ∨ ¬Hostile(z) |
| 2 | R1 and C4 | R2: ¬Weapon(y) ∨ ¬Sells(John,y,z) ∨ ¬Hostile(z) | |
| 3 | R2 and C7 | x/y (in C7) | R3: ¬Missile(y) ∨ ¬Sells(John,y,z) ∨ ¬Hostile(z) |
| 4 | R3 and C5 | y/M1 | R4: ¬Sells(John,M1,z) ∨ ¬Hostile(z) |
| 5 | R4 and C3 | x/M1, z/Abc | R5: ¬Missile(M1) ∨ ¬In(M1,Abc) ∨ ¬Hostile(Abc) |
| 6 | R5 and C5 | R6: ¬In(M1,Abc) ∨ ¬Hostile(Abc) | |
| 7 | R6 and C6 | R7: ¬Hostile(Abc) | |
| 8 | R7 and C8 | x/Abc | R8: ¬Enemy(Abc, America) |
| 9 | R8 and C2 | R9: empty clause (□) |
¬Criminal(John) + C1 -> R1
R1 + C4 (American) -> R2
R2 + C7 (Missile -> Weapon) -> R3
R3 + C5 (Missile(M1)) -> R4
R4 + C3 (sold by John) -> R5
R5 + C5, C6 -> R7: ¬Hostile(Abc)
R7 + C8 (Enemy -> Hostile) -> R8: ¬Enemy(Abc,America)
R8 + C2 -> □
The empty clause is derived, so the negated goal is false and Criminal(John) is true: John is a criminal.
✓ 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: horse, Bluebeard, Charlie · Artificial Intelligence, chapter 4
- Resolution: oversmart persons, Ram · Artificial Intelligence, chapter 4
- Resolution: Marcus and Caesar · Artificial Intelligence, chapter 4
- Resolution: Tuesday test argument · Discrete Structure, chapter 1
- Suspension bridge triangle ABC; span AB · Surveying I, chapter 7
- Circle ABC lies on a cone · Mathematics, chapter 3
- Advantages of abc to dq0 transformation · Electric Machines II, chapter 1