A *clause* is a set of literals. The formula associated with a
clause is the disjunction of the literals in the set. For example, the
clause
has the associated formula
.

A *clause set* is a set of clauses. The formula associated with a
clause set is the conjunctions of the formulas associated with the
clauses in the set. For example, the clause set
has
the associated formula
.

Resolution is a deduction system with just one rule:

Resolution is a *refutation* proof procedure, that is, it is used
to show that a formula is unsatisfiable by deriving from the
formula. Thus, to prove a formula valid by resolution, one:

- Negates the formula to be proved.
- Uses the above procedure find a formula in CNF that is unsatisfiable if and only if the negated formula is unsatisfiable.
- Converts the new formula to a set of clauses.
- Resolves until is found (or no new clauses can be generated).

We show that resolution is both sound and complete.

**Resolution is sound:** First, we prove the following lemma.

**Lemma: ** If the clause
that results from one application of the
resolution rule is false under a valuation , then the conjunction
of the hypotheses of the rule,
, is false under .

**Proof: ** Suppose that is false under , but the
is true under . Since is a disjunction, one of its
literals must be true under . If the literal is some literal other
than , then that literal is also in , and so is true, which
is a contradiction. On the other hand, if that literal is , then
is false under . Since is true under , it must
contain a literal other than which is true under . But
that literal also occurs in , and so is true under - again,
a contradiction. Thus,
must be false under .

By induction (on the number of resolutions steps), we can show that if we can derive a clause that is false under a valuation , then the conjunction of premises must be false under . So, if we can derive (which is false under all valuations) using resolution, the conjunction of the premises is false under all valuations, hence is unsatisfiable.

**Resolution is complete:** To show that resolution is complete, we
will use an induction proof. However, the tricky part of the proof is
what we induct on. We create a new measure, the *number of excess
literals,* for this purpose.

The *number of excess literals* in a clause is defined to be the
number of literals, excluding the first one (if there is a first one)
in the clause. That is,

The number of excess literals in a clause set is just the sum of excess literals in all the clauses, i.e., .

**Theorem:** If an unsatisfiable set of clauses, , has excess
literals, then we can derive from the set using resolution.

**Proof:** The base case is when . In this case, all clauses
must have 0 excess literals. So each clause must have 0 or 1
literals. If some clause has no literals, then that clause must be
, and so we have the resolution proof where is a premise.
On the other hand, if all clauses have exactly one literal and the set
is unsatisfiable, it must be the case that the set contains a clause
with just the literal and a clause with just its negation, (or some ). We can resolve these two clauses in one resolution
step to produce . In either case, we have a resolution proof of
.

Now suppose that and that the theorem is true for every
unsatisfiable set of clauses with fewer than excess literals. We
will construct an unsatisfiable set of clauses with fewer literals and
use its proof of to construct a proof for . Since has
excess literals, some clause in must contain an excess
literal. Call such an excess literal . We create a new clause set,
from by deleting from every clause in which it appears and
also by deleting *every clause* which contains from the
set. Clearly, has less than excess literals since at least
one instance of the excess literal was deleted. We next show that
is unsatisfiable.

Suppose that is satisfiable and that is a valuation that makes true. We extend to by setting to be false. Now, consider each clause, , in . If contains , then it is true under since is false under . If doesn't contain , then it corresponds to a clause, in (possibly with the literal deleted). But is true under and is a subset of . Thus is true under as well. Thus satisfies , a contradiction as is unsatisfiable. Thus is also unsatisfiable.

Since is unsatisfiable and has fewer than excess literals, we can apply the theorem to it. Thus, we can find a resolution proof of from . We now do the same proof using the original clauses from as premises and doing the same resolution steps. The only difference between this and the original proof is that some clauses may now contain the literal . If one or both hypotheses of a resolution step contain then the conclusion will also contain , and thus this additional literal may be propagated through the proof. Thus, we can show by induction on the number of resolution steps that the conclusion of the new proof is either (if none of the premises used in the original proof correspond to clauses of which contain ), or (otherwise). Thus, we can produce the clause or by resolution from .

If the new proof results in , we are done. Otherwise, we have a little more work to do. We create another new clause set, by deleting the literal from the clauses of and removing any clause that contains . Since at least one clause with the excess literal has been deleted, has fewer than excess literals, and by an argument symmetric to the one above, is unsatisfiable. Thus, again by induction, we can derive from using resolution. Each premise of this new proof is either a clause of , or a clause of from which the literal has been deleted. In the latter case, we can derive the new premise from the corresponding original clause, by resolving the original clause with the clause from the previous proof. Thus, all premises of the derivation of from are either members of or can be derived from . Putting these derivations together with this last proof yields a derivation of from the clauses of .