## § 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`

!