Resolution Theorem Proving

Resolution produces proofs by

1. Converting problems into a canonical form. All axioms are converted to clauses in Conjunctive Normal Form.

2. Using refutation - ie, by attempting to show that the negated assertion produces a contradiction with known axioms in the database. This requires using the resolution inference rule and unification.

To prove a theorem using resolution:

1. negate the theorem to be proved and add the result to the list of axioms
2. put axioms into clause form
3. Until the empty clause, Nil, is produced or there is no resolvable pair of clauses, find resolvable clauses, resolve them and add the result to the list of clauses
4. if the empty clause is produced, report that the theorem is TRUE. If there are no resolvable clauses, report that the theorem is FALSE.

<<<Previous Section Next>>>