## § Resolution algorithm for propositional logic

- Resolution is refutation complete: will find a disproof if one exists for propositional logic
- Key idea is the resolution rule:

```
F \/ l; G \/ not(l)
-------------------
F \/ G
```

- See that this allows us to reduce the number of occurrences of
`l`

. If we keep doing this, we get the empty set with `\/`

as the monoidal operation, forcing us to conclude `False`

.

#### § Termination

- At each step, we introduce a new clause, but the clause has one fewer literal.
- So we decrease on the number of literals this clause can resolve with.

#### § Soundness

- First node that the resolution rule is sound, in that it only infers correct clauses.
- See that we need to prove only one rule:
`(X | A) & (!X | B) = (A & B)`

, which can be proven by e.g. truth table. - So if resolution finds a contradiction, the original set of cluases did have a contradiction.

#### § Completeness

- We need to show that if resolution did not find a contradiction, then a model exists (the set of clauses was consistent)
- Suppose resolution saturates, and did not find a contradiction.
- Then we claim that in this saturated set, every literal
`L`

either occurs as all positive, or all negative, or does not occur. - If this is true, then clearly we have a model: for every +ve literal, assign true, for every pure -ve literal, assign false, for a literal that does not occur, assign it whichever.
- Suppose the claim is not true. Then a literal L occurs in some clause C as +ve, and in another clause C' as negative.
- This means that C, C' can be resolved to get a new clause!
- But this cannot be, since we assumed that the set of clauses was saturated.