Resolution[J. A. Robinson, A machine oriented logic based
on the resolution principle, * Journal of the ACM*, ** 12**, No. 1, 1965.]
is a method of proof by contradiction.

Given a set of premises *F _{1} &and F_{2} &and ... &and F_{n}*
and a desired conclusion

Theorem: If *H* is a logical consequence of *F*, * F &and H = F*.
Proof: If *F* is false, then both sides are false. If *F* is true, then
*H* must be true, so *F &and H* is true.

Thus, we are justified in adding any logical consequence of our set of formulas to the set without changing its truth value.