Resolution

Resolution theorem proving is a method of formal derivation (deduction) that has the following features:
• The only formulas allowed in resolution theorem proving are disjunctions of literals.
• A disjunction of literals is called a clause. Hence, all formulas involved in resolution theorem proving must be clauses.
• Resolution follows the refutation principle; that is, it shows that the negation of the conclusion is inconsistent with the premises.
• There is essentially only one rule of formal deduction, resolution.
In general, one can convert any formula into one or more clauses.
• To do this, one rst converts the formula into a conjunction of disjunctions; that is, one converts the formula into conjunctive normal form.
• Each term of the conjunction is then made into a clause of its own.
Two clauses can be resolved if and only if they contain two complementary literals.
• In this case, they give rise to a new clause, called the resolvent.
• If the complementary literals are P and ~P, one says the resolution in on P (or over P).
• The clauses giving rise to the resolvent are called parent clauses.
• The resolvent on P is the disjunction of all literals of the parent clauses, except that P and ~P are omitted from the resolvent. A
The resolvent is logically implied by its parent clauses, which makes resolution a sound rule of formal deduction. To see this, let P be a propositional variable, and let A and B be (possibly empty) clauses. One has P v A, ~P v B = A v B This is valid for the following reasons:-
•if P is false, then A must be true, because otherwise P v A is false.
• Similarly, if P is true, then B must be true, because otherwise ~P v B is false.
• Since P must be true or false, either A or B must be true, and the result follows.
• Of course, A v B is the resolvent of the parent clauses P v A and ~P v B on P, which proves the soundness of resolution.
Soundness of resolution