Questions: Propositional Resolution

Question 1

You want to use propositional resolution to prove that formula φ follows from premises Γ. What is the correct procedure?

• A. Convert φ to CNF and resolve its clauses until you derive each clause of Γ
• B. Add ¬φ to Γ, convert everything to CNF, and resolve until the empty clause ⊥ is derived
• C. Convert both φ and Γ to CNF separately and check whether every clause of φ appears in Γ
• D. Resolve the clauses of Γ together until either φ or ¬φ is derived

Answer: (B)

Resolution is a *refutation* system — it proves things by deriving contradiction, not by constructing proofs forward. To show Γ ⊨ φ, you negate what you want to prove (add ¬φ to Γ), convert everything to CNF, and apply the resolution rule repeatedly. If you derive the empty clause ⊥, you have shown that Γ ∧ ¬φ is unsatisfiable — meaning there is no world where Γ is true and φ is false — which is exactly what Γ ⊨ φ means. Attempting to derive φ directly from Γ (option D) doesn't work because resolution as a rule produces clauses, not arbitrary formulas.

Question 2

Applying resolution to clauses (A ∨ B ∨ ¬C) and (C ∨ D), where C is the resolved literal, produces which resolvent?

• A. (A ∨ B ∨ D)
• B. (A ∨ B ∨ ¬C ∨ C ∨ D)
• C. (A ∨ B)
• D. (¬C ∨ C)

Answer: (A)

The resolution rule: from (X ∨ p) and (Y ∨ ¬p), derive (X ∨ Y). Here the complementary pair is ¬C and C. Remove both from their respective clauses and combine the remaining literals: (A ∨ B) from the first clause and (D) from the second, giving (A ∨ B ∨ D). Option B is wrong — it includes both C and ¬C in the resolvent (the whole point is that they cancel). Option C drops D. Option D is a tautology (always true) and is never a valid resolvent from these clauses.

Question 3

If propositional resolution derives the empty clause from a set of clauses, this proves that the clause set is satisfiable.

• T. True
• F. False

Answer: False

The opposite is true. The empty clause ⊥ has no literals — it is a disjunction of zero things, which is vacuously false (a contradiction). Deriving ⊥ means the clause set is *unsatisfiable*: there is no truth assignment that makes all clauses simultaneously true. Resolution is a refutation proof system: it proves unsatisfiability, not satisfiability. If you want to prove that a formula φ follows from premises Γ, you *negate* φ and try to derive ⊥, showing that Γ ∧ ¬φ is unsatisfiable — and therefore φ must be true whenever Γ is.

Question 4

Resolution is refutation-complete: if a set of propositional clauses is unsatisfiable, there always exists a finite sequence of resolution steps that derives the empty clause.

• T. True
• F. False

Answer: True

Refutation completeness is resolution's central theoretical guarantee. It means that if no truth assignment satisfies all the clauses, then resolution *can* find a derivation of ⊥ — it won't miss an unsatisfiable instance. However, refutation completeness does not mean resolution is efficient: the number of resolution steps may be exponential. Nor does it help with satisfiable instances — if the clause set is satisfiable, resolution will never derive ⊥ (since no contradiction exists), but it also doesn't produce a satisfying assignment directly. Modern SAT solvers address the efficiency gap with conflict-driven clause learning and other heuristics built on top of the resolution foundation.

Question 5

Why do automated theorem provers using resolution negate the goal formula before resolving, rather than trying to derive the goal directly from the premises?

Model answer: Resolution is a refutation system — its only mechanism is deriving the empty clause ⊥, which represents a contradiction. It has no rule for directly constructing a proof that a formula is true. To prove Γ ⊨ φ, we use the logical equivalence: Γ ⊨ φ if and only if Γ ∧ ¬φ is unsatisfiable. By adding ¬φ to Γ and converting to CNF, we ask: 'can we find a contradiction in this expanded set?' If resolution derives ⊥, the answer is yes — and that contradiction proves φ must be true whenever Γ holds.

This is proof by contradiction mechanized. It works because of the soundness and refutation-completeness of resolution: if Γ ∧ ¬φ is genuinely unsatisfiable, resolution will find a derivation of ⊥ (completeness), and any derivation of ⊥ correctly certifies unsatisfiability (soundness). The design elegance is that you need only one inference rule (resolution) and one goal (derive ⊥) to handle all propositional reasoning — no separate rules for 'and-introduction,' 'modus ponens,' etc.