- 2073 Magh · 10 marks
Resolution: Mary loves John
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.
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.
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.
- ∀x loves(Mary,x) → star(x)
- ∀x [student(x) ∧ ¬pass(x)] → ¬play(x)
- student(John)
- ∀x [student(x) ∧ ¬study(x)] → ¬pass(x)
- ∀x ¬play(x) → ¬star(x)
Goal: ¬study(John) → ¬loves(Mary,John)
Step 2: Clause form (remove →, using P → Q ≡ ¬P ∨ Q)
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:
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) |
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.
✓ Answer checked by Claude Opus 5.5 (high effort)
Related questions
- Resolution: John likes peanuts · Artificial Intelligence, chapter 4 · asked 2×
- Resolution: horse, Bluebeard, Charlie · Artificial Intelligence, chapter 4
- Resolution: American sells weapons · Artificial Intelligence, chapter 4 · asked 2×
- Pass student array; display passed students · Computer Programming, chapter 7
- Prove sampling theorem for low pass signals · Signals and Systems, chapter 4
- Resolution: Tuesday test argument · Discrete Structure, chapter 1
- Transmission and y parameters, prove not reciprocal or symmetrical · Electrical Circuit Theory, chapter 7 · asked 2×