Questions: Ground Instances and Variable Instantiation

Question 1

A student claims that to show a set of first-order clauses is unsatisfiable, you must demonstrate that no interpretation over any domain satisfies them. What does Herbrand's theorem tell us instead?

• A. You must check all interpretations whose domain has exactly one element
• B. You only need to find a finite set of ground instances that are propositionally unsatisfiable
• C. You must run the unification algorithm until it reports failure
• D. You must show the clause set has no model of cardinality greater than the number of clauses

Answer: (B)

Herbrand's theorem is a landmark reduction: a set of first-order clauses is unsatisfiable if and only if some *finite* set of ground instances is propositionally unsatisfiable. You never need to reason about all interpretations over arbitrary domains — just ground-instantiate clauses over the Herbrand universe and check them with propositional methods. The other options mistake the theorem for a restriction on model size or for the unification procedure.

Question 2

Unification finds the most general substitution making two terms syntactically identical. Ground instantiation is best understood as the conceptual opposite because it:

• A. Finds the least specific substitution that makes two clauses match
• B. Replaces every free variable with a specific ground term from the Herbrand universe
• C. Converts clauses to conjunctive normal form before any substitution
• D. Checks whether a formula is propositionally valid by enumeration

Answer: (B)

Unification makes the minimal commitment — it leaves as much generality as possible (the most general unifier). Ground instantiation makes the maximal commitment — every variable is replaced by a fully concrete term with no variables. In automated theorem proving, unification is used to intelligently select which ground instances to generate, avoiding the need to enumerate all of the (potentially infinite) Herbrand universe.

Question 3

A ground term contains no variables, so it can be evaluated as true or false in a model without providing any variable assignment.

• T. True
• F. False

Answer: True

This is the defining property of ground terms. A ground formula requires no variable assignment to evaluate because all positions are filled by specific constants or function applications built from constants — there is nothing left to bind. This is why ground instances are the bridge from first-order to propositional reasoning: they are already concrete enough to be checked by propositional methods.

Question 4

The Herbrand universe of a clause set is the set of most interpretations (models) that satisfy most clause in the set.

• T. True
• F. False

Answer: False

The Herbrand universe is a *syntactic* object, not a set of models. It is the set of all ground terms constructible from the constants and function symbols that appear in the clause set (adding a dummy constant if none appear). It defines the possible substitutions for variables when generating ground instances. A Herbrand *interpretation* is an interpretation whose domain is the Herbrand universe — but the universe itself is just a domain of ground terms.

Question 5

What is the significance of Herbrand's theorem for automated theorem proving, and how does it allow first-order reasoning to be reduced to propositional reasoning?

Model answer: Herbrand's theorem says a set of first-order clauses is unsatisfiable iff some finite subset of its ground instances is propositionally unsatisfiable. This allows theorem provers to sidestep quantifiers and arbitrary domains entirely: instead of reasoning about all possible structures, they generate ground instances over the Herbrand universe and check propositional unsatisfiability. The challenge is choosing which instances to generate — this is where unification is essential, since it identifies which substitutions will produce resolving pairs.

The reduction is powerful because propositional satisfiability checking, while NP-complete, has highly effective algorithms (DPLL, CDCL), whereas first-order reasoning is only semi-decidable. Herbrand's theorem guarantees that if a refutation exists, a finite propositional witness exists — but it does not guarantee termination if the clause set is satisfiable, which is consistent with first-order logic being undecidable.