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