Logic and Proof MT24, Ground resolution

Created: November 26, 2024 | Updated: March 26, 2025 | About these notes | View in context | Study these flashcards

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

Ground resolution theorem

@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)$.
\[\begin{aligned} F \text{ unsatisfiable} &\stackrel{(1)}{\iff} E(F) \text{ unsatisfiable as set of propositional formulas} \\\\ &\stackrel{(2)}{\iff} \text{finite subset of }E(F) \text{ is unsatisfiable} \\\\ &\stackrel{(3)}{\iff} \text{can derive }\square \text{ from } E(F) \text{ using resolution} \end{aligned}\]

where each of the equivalences are established by:

  • (1): Herbrand’s theorem
  • (2): Compactness theorem
  • (3): Soundness and completeness of propositional resolution

Examples

Use ground resolution to show that the conjunction of all these sentences is unsatisfiable:

  1. Everyone is similar to themself.
  2. Everyone is worshipped by all their fans.
  3. Everyone has a fan whom they respect.
  4. Nobody who worships anyone similar to Oscar is respected by Oscar.

In first-order logic:

  1. $\forall x \text{ } S(x, x)$
  2. $\forall x \forall y \text{ } (F(x, y) \to W(x, y))$
  3. $\forall x \exists y \text{ } (F(y, x) \land R(x, y))$
  4. $\forall x \forall y \text{ } (S(y, \text{O}) \land W(x, y) \to \lnot R(\text{O}, x))$

In Skolem form:

  1. $\forall x \text{ } S(x, x)$
  2. $\forall x \forall y \text{ } (\lnot F(x, y) \lor W(x, y))$
  3. $\forall x \text{ } (F(f(x), x) \land R(x, f(x)))$
  4. $\forall x \forall y \text{ } (\lnot S(y, \text{O}) \lor \lnot W(x, y) \lor \lnot R(\text{O}, x))$

Then, using ground resolution:

  1. $S(\text{O}, \text{O})$ (Ground1)
  2. $\lnot S(\text{O}, \text{O}) \lor \lnot W(f(\text{O}), \text{O}) \lor \lnot R(\text{O}, f(\text{O}))$ (Ground4)
  3. $\lnot W(f(\text{O}), \text{O}) \lor \lnot R(\text{O}, f(\text{O}))$ (Res1,2)
  4. $R(\text{O}, f(\text{O}))$ (Ground3)
  5. $\lnot W(f(\text{O}), \text{O})$ (Res3,4)
  6. $\lnot F(f(\text{O}), \text{O}) \lor W(f(\text{O}), \text{O})$ (Ground2)
  7. $\lnot F(f(\text{O}), \text{O})$ (Res5,6)
  8. $F(f(\text{O}), \text{O})$ (Ground3)
  9. $\square$ (Res7,8)

@example~ @exam~



Related posts