Questions: First-Order Resolution

Question 1

In first-order resolution, why do we negate the conclusion and add it to the premises before attempting to derive the empty clause?

• A. To convert the formula into clause normal form, which is required before Skolemization can proceed
• B. Because resolution works by refutation: if the premises plus the negated conclusion lead to contradiction, then the conclusion must logically follow from the premises
• C. To allow unification to match complementary literals in the goal with literals in the premises
• D. Because resolution cannot handle positive literals — only negated literals can be resolved

Answer: (B)

First-order resolution is a proof by contradiction. If a conclusion C follows from premises P, then P ∧ ¬C is unsatisfiable — there is no model that satisfies all premises while also falsifying the conclusion. By adding ¬C to the clause set and trying to derive □ (the empty clause, representing contradiction), we are proving that no such model exists. If we succeed, C must be true in every model of P. This refutation strategy is what makes resolution a complete proof procedure for first-order logic.

Question 2

A student runs a first-order resolution prover on a satisfiable set of first-order clauses (no logical contradiction exists). After an hour, the prover has not terminated. The student concludes the prover has a bug. Is this correct?

• A. Yes — any correct theorem prover must terminate in polynomial time on finite inputs
• B. No — first-order resolution is refutation-complete but not a decision procedure; on satisfiable inputs where no contradiction exists, the prover may run forever because first-order validity is only semidecidable
• C. Yes — the prover is in an infinite loop caused by incorrect unification
• D. No — but only because the input must actually be unsatisfiable, and the prover will eventually find the refutation

Answer: (B)

There is no general algorithm that can decide, for arbitrary first-order formulas, whether a proof exists. If an input is unsatisfiable, refutation-completeness guarantees the prover will eventually find the empty clause. But if the input is satisfiable, the prover may generate new resolvents indefinitely — it has no way to know that no contradiction will ever appear. This is a fundamental theoretical limit (undecidability of first-order validity), not a bug. Decidable fragments exist (propositional logic, some restricted first-order fragments), but general first-order resolution cannot avoid this.

Question 3

Skolemization preserves logical equivalence: the Skolemized version of a formula is true in exactly the same models as the original.

• T. True
• F. False

Answer: False

Skolemization preserves satisfiability, not logical equivalence. The Skolemized formula is equisatisfiable — it is satisfiable if and only if the original is — but the models of the two formulas are generally different. Skolem functions introduce new function symbols that don't appear in the original language, so they can't be models of the original formula. This is sufficient for refutation proofs (we only need to know whether the clause set is unsatisfiable), but it means you cannot interpret Skolem terms as actual witnesses in the original formula's semantics.

Question 4

If a set of first-order clauses is unsatisfiable, first-order resolution is guaranteed to find a refutation (derive the empty clause) in finite time.

• T. True
• F. False

Answer: True

This is what 'refutation-complete' means. Herbrand's theorem provides the theoretical basis: an unsatisfiable set of first-order clauses has a finite unsatisfiable set of ground instances, which has a propositional resolution refutation. The resolution procedure, by systematically generating ground instances and resolving them, will eventually find this finite refutation. The key asymmetry is that completeness is guaranteed only for the unsatisfiable case — the satisfiable case may not terminate.

Question 5

Explain why first-order resolution is described as 'refutation-complete but undecidable,' and what this means in practice when running an automated theorem prover.

Model answer: Refutation-complete means: if a conclusion follows from premises (the negated conclusion plus premises is unsatisfiable), the resolution procedure will eventually derive the empty clause and confirm the proof. No valid proof will be missed. Undecidable means: if the input is satisfiable (no contradiction exists), there is no guaranteed termination — the prover may generate resolvents indefinitely without being able to conclude 'no proof exists.' In practice, provers use search strategies (ordering heuristics, clause deletion, depth limits) to handle non-termination, but they cannot solve the fundamental problem: an incomplete run doesn't tell you whether a proof would eventually appear or simply doesn't exist. Prover9 and Prolog (via SLD-resolution) are both built on this foundation, so they share the same theoretical limitation.

The contrast with propositional resolution is instructive: propositional logic is decidable because the clause set is finite and no new distinct clauses can be generated indefinitely. First-order resolution can generate infinitely many ground instances via Herbrand expansion, so the search space is infinite in the satisfiable case.