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
-
Convert all the propositions of a knowledge base KB to clause normal form (CNF)
-
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.
-
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.
