Skip to main content

Resolution: cup supports book

Short answer

Convert to FOPL clauses, negate goal ¬Supports(Book,Cup). Resolve with C1: ¬OnTop(Cup,Book); with C2: ¬Above(Cup,Book) ∨ ¬Touching(Cup,Book); with C3: ¬Touching(Cup,Book); with C4: empty clause. Contradiction proves Supports(Book,Cup) true.

If X is on the top of Y, Y supports X. If X is above Y and they are touching each other, X is on the top of Y. A cup is above a book. A cup is touching a book. Show that supports (book, cup) is true.

Step 1: Statements in FOPL

Predicates: OnTop(x,y), Supports(x,y) = x supports y, Above(x,y), Touching(x,y).

  1. ∀x ∀y OnTop(x, y) → Supports(y, x)
  2. ∀x ∀y [Above(x, y) ∧ Touching(x, y)] → OnTop(x, y)
  3. Above(Cup, Book)
  4. Touching(Cup, Book)

Goal: Supports(Book, Cup)

Step 2: Clauses

No.Clause
C1¬OnTop(x, y) ∨ Supports(y, x)
C2¬Above(x, y) ∨ ¬Touching(x, y) ∨ OnTop(x, y)
C3Above(Cup, Book)
C4Touching(Cup, Book)

Step 3: Negated goal

C5: ¬Supports(Book, Cup)

Step 4: Resolution

StepResolveSubstitutionResolvent
1C5 and C1y/Book, x/CupR1: ¬OnTop(Cup, Book)
2R1 and C2x/Cup, y/BookR2: ¬Above(Cup, Book) ∨ ¬Touching(Cup, Book)
3R2 and C3R3: ¬Touching(Cup, Book)
4R3 and C4R4: empty clause (□)
¬Supports(Book,Cup) + C1 -> ¬OnTop(Cup,Book)
   + C2 -> ¬Above(Cup,Book) ∨ ¬Touching(Cup,Book)
   + C3 -> ¬Touching(Cup,Book)
   + C4 -> □

The empty clause is obtained, so the assumption is false. Hence Supports(Book, Cup) is true.

✓ Answer checked by Claude Opus 5.5 (high effort)

Related questions

All Artificial Intelligence chapter 4 questions →