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.
Convert all the propositions of a knowledge base
clause normal form
(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
b) Resolve them together using the
. The resolvent will be the disjunction of all the literals of both parent clauses with appropriate substitutions.
c) If the resolvent is the
, then a contradiction has been found. If it is not, then add it to the set of clauses available to the procedure.
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License