--- title: "Resolution: American sells weapons" subject: "Artificial Intelligence" chapter: 4 key: "semester_6/artificial_intelligence:resolution-american-criminal" source: https://www.bctengineer.com/q/semester_6/artificial_intelligence/resolution-american-criminal site: BCT Engineering --- # Resolution: American sells weapons Artificial Intelligence · Chapter 4: Knowledge Representation, Inference & Reasoning - Asked in: 2069 Bhadra, 10 marks; 2075 Baisakh, 8 marks (asked 2 times) - Video: [14 Proof by Resolution First Order Logic Solved Example Artificial Intelligence Mahesh Huddar Part 1](https://www.youtube.com/watch?v=nEEyPdYxBFY) — Mahesh Huddar - Answer checked by Claude Opus 5.5 (high effort) on 2026-10-14 - Page: https://www.bctengineer.com/q/semester_6/artificial_intelligence/resolution-american-criminal - Whole chapter: https://www.bctengineer.com/md/semester_6/artificial_intelligence/chapter-4 ## Question 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. ## 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. ## Answer #### 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. 1. ∀x ∀y ∀z [American(x) ∧ Weapon(y) ∧ Sells(x,y,z) ∧ Hostile(z)] → Criminal(x) 2. Enemy(Abc, America) 3. ∀x [Missile(x) ∧ In(x, Abc)] → Sells(John, x, Abc) 4. 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 (□)** | ```text ¬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.** ## Check yourself The answer's key points as multiple-choice questions, with the correct option and why. 1. In resolution refutation, what is added to the clauses before resolving? A. The goal itself B. The negation of the goal C. Nothing D. A random clause Answer: B. We add ¬Criminal(John) and derive the empty clause to show a contradiction. (Key point: Refutation method) 2. Which common-sense assumptions were needed besides the stated premises? A. Missile(M1) with In(M1,Abc), Missile(x) → Weapon(x), and Enemy(x,America) → Hostile(x) B. Only that John is rich C. Criminal(Abc) D. Nothing, the premises alone suffice Answer: A. The proof needs Abc to have a missile, missiles to be weapons, and enemies of America to be hostile. (Key point: Needed background facts) 3. Resolving C1 with ¬Criminal(John) uses which substitution? A. x/Abc B. x/John C. x/M1 D. z/John Answer: B. Unifying Criminal(x) with Criminal(John) binds x to John. (Key point: Key substitution) 4. What does deriving the empty clause show? A. The negated goal is false, so Criminal(John) is true B. The knowledge base is empty C. John is innocent D. The proof failed Answer: A. The empty clause is a contradiction, so the negated goal cannot hold and John is a criminal. (Key point: Conclusion) ## 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: horse, Bluebeard, Charlie](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Aresolution-horses-charlie) — Artificial Intelligence, chapter 4 - [Resolution: oversmart persons, Ram](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Aresolution-oversmart-ram-naughty) — Artificial Intelligence, chapter 4 - [Resolution: Marcus and Caesar](https://www.bctengineer.com/question.md?key=semester_6%2Fartificial_intelligence%3Aresolution-pompeian-caesar) — Artificial Intelligence, chapter 4 ## Related in other subjects - [Resolution: Tuesday test argument](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Aresolution-tuesday-discrete-structure) — Discrete Structure, chapter 1 - [Suspension bridge triangle ABC; span AB](https://www.bctengineer.com/question.md?key=semester_3%2Fsurveying_i%3Asuspension-bridge-triangle-abc-span-ab) — Surveying I, chapter 7 - [Circle ABC lies on a cone](https://www.bctengineer.com/question.md?key=semester_2%2Fmathematics%3Acircle-abc-lies-cone) — Mathematics, chapter 3 - [Advantages of abc to dq0 transformation](https://www.bctengineer.com/question.md?key=semester_5%2Felectric_machines_ii%3Aabc-dq0-transformation) — Electric Machines II, chapter 1