Notes - Logic and Proof MT24, Ground resolution
The ground resolution theorem establishes a way to use the soundness and completeness of propositional resolution ( [[Notes - Logic and Proof MT24, Propositional resolution]]U) in order to prove unsatisfiability of first-order formulas by passing to the Herbrand expansion.
[[Notes - Logic and Proof MT24, Unification and resolution]]U avoids the need to work out the Herbrand expansion and instead gives a procedure that works directly on first-order formulas, avoiding the need to convert it to a propositional problem.
Flashcards
@State the ground resolution theorem.
Suppose:
- $F$ is closed formula in Skolem form
- $E(F)$ is the corresponding Herbrand expansion
Then:
- $F$ is unsatisfiable iff there is a propositional resolution proof of $\square$ from $E(F)$.
(in other words, the ground resolution theorem is like the completeness theorem for propositional resolution refutations).
@Prove, by appealing to other results, the ground resolution theorem, i.e. if
- $F$ is closed formula in Skolem form
- $E(F)$ is the corresponding Herbrand expansion
Then:
- $F$ is unsatisfiable iff there is a propositional resolution proof of $\square$ from $E(F)$.
By the compactness theorem for propositional logic, $E(F)$ is unsatisfiable iff there is some finite subset of $E(F)$ that is unsatisfiable.
By the soundness and completeness of propositional resolution, this holds iff we can derive $\square$ from $E(F)$ using resolution.