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.