--- title: "Resolution: Mary loves John" subject: "Artificial Intelligence" chapter: 4 key: "semester_6/artificial_intelligence:resolution-mary-john-football" source: https://www.bctengineer.com/q/semester_6/artificial_intelligence/resolution-mary-john-football site: BCT Engineering --- # Resolution: Mary loves John Artificial Intelligence · Chapter 4: Knowledge Representation, Inference & Reasoning - Asked in: 2073 Magh, 10 marks - Video: [Resolution to Prove Predicate Facts to First Order Logic FOL Artificial Intelligence Mahesh Huddar](https://www.youtube.com/watch?v=CbI-Q2a5rUU) — 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-mary-john-football - Whole chapter: https://www.bctengineer.com/md/semester_6/artificial_intelligence/chapter-4 ## Question Consider the following axioms: i) Anyone whom Mary loves is a football star. ii) Any student who does not pass does not play. iii) John is a student. iv) Any student who does not study does not pass. v) Anyone who does not play is not a football star. Prove that "If John does not study, then Mary does not love John" using resolution by refutation. ## Short answer Convert axioms to clauses, add negated goal clauses ¬study(John) and loves(Mary,John). Resolution chain from loves yields star(John), play(John), pass(John), then study(John), clashing with ¬study(John) to give NIL. Thus if John doesn't study, Mary doesn't love him. ## Answer **Method:** convert every axiom to first-order logic, then to clause form, add the negation of the goal, and resolve until the empty clause (NIL) appears. #### Step 1: Axioms in FOPL Predicates: loves(x,y), star(x) = x is a football star, student(x), pass(x), play(x), study(x). Constants: Mary, John. 1. ∀x loves(Mary,x) → star(x) 2. ∀x [student(x) ∧ ¬pass(x)] → ¬play(x) 3. student(John) 4. ∀x [student(x) ∧ ¬study(x)] → ¬pass(x) 5. ∀x ¬play(x) → ¬star(x) **Goal:** ¬study(John) → ¬loves(Mary,John) #### Step 2: Clause form (remove →, using P → Q ≡ ¬P ∨ Q) ```text C1: ¬loves(Mary,x) ∨ star(x) C2: ¬student(x) ∨ pass(x) ∨ ¬play(x) C3: student(John) C4: ¬student(x) ∨ study(x) ∨ ¬pass(x) C5: play(x) ∨ ¬star(x) ``` (Axiom 5: ¬(¬play) ∨ ¬star = play ∨ ¬star.) #### Step 3: Negate the goal ¬[¬study(John) → ¬loves(Mary,John)] ≡ ¬study(John) ∧ loves(Mary,John). This gives two clauses: ```text C6: ¬study(John) C7: loves(Mary,John) ``` #### Step 4: Resolution refutation | Step | Resolve | Unifier | Resolvent | |---|---|---|---| | C8 | C7 and C1 | x = John | star(John) | | C9 | C8 and C5 | x = John | play(John) | | C10 | C9 and C2 | x = John | ¬student(John) ∨ pass(John) | | C11 | C10 and C3 | none | pass(John) | | C12 | C11 and C4 | x = John | ¬student(John) ∨ study(John) | | C13 | C12 and C3 | none | study(John) | | C14 | C13 and C6 | none | NIL (empty clause) | ```text C7 loves(M,J) C1 ¬loves(M,x)∨star(x) \ / C8 star(J) C5 play(x)∨¬star(x) \ / C9 play(J) C2 ¬student∨pass∨¬play \ / C10 ¬student(J)∨pass(J) C3 student(J) \ / C11 pass(J) C4 ¬student∨study∨¬pass \ / C12 ¬student(J)∨study(J) C3 \ / C13 study(J) C6 ¬study(J) \ / NIL ``` #### Conclusion The set of axioms plus the negated goal gives the empty clause, so it is unsatisfiable. Hence the goal is true: **if John does not study, then Mary does not love John.** ## Check yourself The answer's key points as multiple-choice questions, with the correct option and why. 1. What does the negation of 'if ¬study(John) then ¬loves(Mary,John)' give? A. study(John) ∨ ¬loves(Mary,John) B. ¬study(John) ∨ loves(Mary,John) C. ¬study(John) ∧ loves(Mary,John), as two clauses D. study(John) ∧ loves(Mary,John) Answer: C. ¬(A → B) ≡ A ∧ ¬B, so both ¬study(John) and loves(Mary,John) become clauses. (Key point: Negating the goal) 2. Which is the clause form of 'any student who does not pass does not play'? A. ¬student(x) ∨ pass(x) ∨ ¬play(x) B. ¬student(x) ∨ ¬pass(x) ∨ ¬play(x) C. student(x) ∨ pass(x) ∨ play(x) D. ¬student(x) ∨ pass(x) ∨ play(x) Answer: A. student ∧ ¬pass → ¬play becomes ¬student ∨ pass ∨ ¬play. (Key point: Axiom 2 clause) 3. What is the order of facts derived from loves(Mary,John)? A. play(John), star(John), pass(John), study(John) B. star(John), play(John), pass(John), study(John) C. star(John), pass(John), play(John), study(John) D. pass(John), star(John), study(John), play(John) Answer: B. Loves gives star; star gives play; play gives pass; pass gives study. (Key point: Chain of derivation) 4. Why does the empty clause (NIL) prove the goal? A. Because study(John) was an axiom B. Because the axioms alone are contradictory C. Because pass(John) was assumed D. study(John) contradicts the assumed ¬study(John), so the negated goal is false Answer: D. Axioms plus negated goal are unsatisfiable, so the goal follows from the axioms. (Key point: Contradiction) ## 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: 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× ## Related in other subjects - [Pass student array; display passed students](https://www.bctengineer.com/question.md?key=semester_1%2Fcomputer_programming%3Apass-whole-array-student-info) — Computer Programming, chapter 7 - [Prove sampling theorem for low pass signals](https://www.bctengineer.com/question.md?key=semester_4%2Fsignals_and_systems%3Asampling-theorem-lowpass) — Signals and Systems, chapter 4 - [Resolution: Tuesday test argument](https://www.bctengineer.com/question.md?key=semester_4%2Fdiscrete_structure%3Aresolution-tuesday-discrete-structure) — Discrete Structure, chapter 1 - [Transmission and y parameters, prove not reciprocal or symmetrical](https://www.bctengineer.com/question.md?key=semester_3%2Felectrical_circuit_theory%3Atransmission-and-y-parameters-neither-reciprocal) — Electrical Circuit Theory, chapter 7, asked 2×