§ 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.