## ยง 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`

.