The resolution principle, due to Robinson (1965), is a method of theorem proving that proceeds by constructing refutation proofs, i.e., proofs by contradiction. This method has been exploited in many automatic theorem provers. The resolution principle applies to first-order logic formulas in Skolemized form. These formulas are basically sets of clauses each of which is a disjunction of literals. Unification is a key technique in proofs by resolution.
If two or more positive literals (or two or more negative literals) in clause 
are unifiable and 
is their most general unifier, then 
is called a factor of 
. For example, 
is factored to 
. In such a factorization, duplicates
are removed.
Let 
and 
be two clauses with no variables in common, let 
contain a positive literal 
, 
contain a negative literal 
, and let 
be the most general unifier of 
and 
. Then
 |
is called a binary resolvent of 
and 
. For example, if 
and 
, then 
is their binary resolvent.
A resolvent of two clauses 
and 
is one of the four following binary resolvents.
1. A binary resolvent of 
and 
.
2. A binary resolvent of 
and a factor of 
.
3. A binary resolvent of a factor of 
and 
.
4. A binary resolvent of a factor of 
and a factor of 
.
Generation of a resolvent from two clauses, called resolution, is the sole rule of inference of the resolution principle. The resolution principle is complete, so a set (conjunction) of clauses is unsatisfiable iff the empty clause can be derived from it by resolution.
Proof of the completeness of the resolution principle is based on Herbrand's theorem. Since unsatisfiability is dual to validity, the resolution principle is exercised on theorem negations.
Multiple strategies have been developed to make the resolution principle more efficient. These strategies help select clause pairs for application of the resolution rule.
For instance, linear resolution is the following deduction strategy. Let 
be the initial set of clauses. If 
, a linear deduction of 
from 
with top clause 
is a deduction in which each 
is a resolvent of 
and 
(
), and each 
is either in 
or a resolvent 
(with 
).
Linear resolution is complete, so if 
is a clause in an unsatisfiable set 
of clauses and 
is satisfiable, then the empty
clause can be obtained by linear resolution with 
as the top clause.
If the additional restriction that 
be in 
imposed, then this restricted strategy is incomplete. However,
it is complete for sets of Horn clauses containing
exactly one goal, and the goal is selected as the
top clause. All other clauses in such sets are definite
Horn clauses. Implementations of programming language
Prolog conduct search within the framework of this strategy.
