ยง 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
.