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 – Complete Resolution Algorithm

  1. Convert all the propositions of a knowledge base KB to clause normal form (CNF)

  2. Negate Q (the to be proven statement) and convert the result to clause form. Add it to the set of clauses obtained in step 1.

  3. Repeat until either a contradiction is found, no progress can be made, or a predetermined amount of effort has been expended:

        a) Select two clauses. Call these the parent clauses.

        b) Resolve them together using the resolution rule . The resolvent will be the disjunction of all the literals of both parent clauses with appropriate substitutions.

        c) If the resolvent is the empty clause , then a contradiction has been found. If it is not, then add it to the set of clauses available to the procedure.


Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.