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