Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

Resolution – Algorithm in Pseudocode

procedure resolution-refutation(KB, Q)
    ;; KB a set of consistent, true sentences
    ;; Q is a goal sentence that we want to derive
    ;; return success if KB ⊢ Q, and failure otherwise
    KB = union(KB, ¬Q)
    while false not in KB do
      pick 2 sentences, S1 and S2, in KB that contain literals that unify
          if none return "failure“
      resolvent = resolution-rule(S1, S2)
      KB = union(KB, resolvnt)
    return "success"

Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.