Resolution Principle
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.
Contact the MathWorld Team
Venn diagram