§ Resolution is Refutation Complete

• Constructive proof.
• We take soundness for granted since it easy by induction on the proof length.
• We prove this by induction on number of literals in the full clausal set. So for a clausal set {{A, B}, {C, D}} our induction measure is 4.

§ One literal

• If we have 1 literal, then our clause set looks like {{A}} which cannot be UNSAT. Thus, we trivially will find a contradiction if one exists.

§ n+1 literals

• Suppose there is assignment that makes the formula UNSAT.
• Then we wish to show that resolution will find False.
• Since we have n+1 literals, there must be at least one clause C that has two literals.
• Let L be one of the literals in clause C. Suppose L occurs as a +ve literal (mutatis mutandis for -ve occurrence.) Write C := C' U { L }, and write the full set of clauses S as S := S' U { C }.
• Note that S' cannot be empty, as we know that S is UNSAT.
• If L does not occur in negative position in any other literal, it can be eliminated from the problem, and we have reduced the number of literals. Use IH to get a resolution contradiction proof of the reduced problem, which is a resolution proof of the original problem.
• Since S := S' U { C } is UNSAT, this means that S' /\ C, or S' /\ (C \/ L) is false. This is to say that (S' /\ C) \/ (S' /\ L) is false, which means that both (S' /\ C) as well as (S' /\ L) is false.
• So, by IH, there must be resolution proofs for both S' U {C} as well as S' U {{L}}.
• Now, consider the resolution DAG for S' U {C}. If {C} is not used in the final derivation of the contradiction, we have a resolution proof using only S'. We can reuse the same resolution proof for S' /\ (C \/ L), so we are done!
• By the exac same argument, we can disregard the case where in the resolution proof in S' U {{L}}, L was not used.
• So now, we have two resolution dags, one with S', {C} |- ... |- False, and one with S', {L} |- ... |- False.
• Recall that we finall want a resolution proof for the clause {C, L}. So what we do is we "percolate" the resolution proof of S', {c} with L, giving us a resolution DAG of the form S', {C, L} |- ... |- L. We then "graft" this tree onto the one with S', {L} |- ... |- False to get the full resolution proof for S', {C, L} |- ... |- False!