Resolution Theorem Proving: Example

• Problem in English:

  Jack owns a dog. Every dog owner is an animal lover. No animal lover kills an animal. Either Jack or Curiosity killed the cat, who is named Tuna. Did Curiosity kill the cat?

• In predicate calculus formulas:

  

• Converting to clause form (and Scheme notation):

  ((dog d))                                                 (1a)
  ((owns jack d))                                           (1b)
  ((~ (dog ?x)) (~ (owns ?x ?y)) (animallover ?x))          (2)
  ((~ (animallover ?z)) (~ (animal ?w)) (~ (kills ?z ?w)))  (3)
  ((kills jack tuna) (kills curiosity tuna))                (4a)
  (cat tuna)                                                (4b)
  ((~ (cat ?u)) (animal ?u))                                (4c)
  

• The goal in clause form:

  ((~ (kills curiosity cat)))                               (5)
  

• Resolutions, using set-of-support strategy
  • Resolving (5) and (4a)

    ((kills jack tuna))                                    (6)
    

  • Resolving (6) and (3)

    ((~ (animallover jack)) (~ (animal tuna)))             (7)
    

  • Resolving (7) and (2)

    ((~ (dog ?v)) (~ (owns jack ?v)) (~ (animal tuna)))    (8)
    

  • Resolving (8) and (1b)

    ((~ (dog d)) (~ (animal tuna)))                        (9)
    

  • Resolving (9) and (1a)

    ((~ (animal tuna)))                                    (10)
    

  • Resolving (10) and (4c)

    ((~ (cat tuna)))                                       (11)
    

  • Resolving (11) and (4b)

    ()
    

• We have found the empty clause and a contradiction; the theorem is proven.
• To answer the question who killed the cat?, we begin with the following goal clause

  ((~ (kills ?q tuna)) (answer ?q))
  

  Then resolution proceeds as before, except that we end up with ((answer curiosity)) in place of the empty clause.