Resolution_2016

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 first 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.
A
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.