Given the terms f(x, g(a)) and f(b, g(y)), what is the most general unifier (MGU)?
A{x ↦ b, y ↦ a, z ↦ c} — binding an extra free variable z to c for completeness
B{x ↦ b, y ↦ a} — binding only what is strictly required to make the terms identical
C{x ↦ a, y ↦ b} — swapping the bindings to match argument positions
DNo unifier exists because f has arguments of different structure in each term
The MGU binds the minimum necessary: x must become b (to match the first arguments: x and b), and y must become a (to match g(a) and g(y): the arguments a and y). Applying {x↦b, y↦a} gives f(b, g(a)) and f(b, g(a)) — identical. Option A adds a binding for z that is unconstrained and unnecessary — it is a valid unifier but not the most general one. The MGU commits the least, leaving all non-required variables free for subsequent inference steps.
Question 2 Multiple Choice
A student argues that for resolution-based theorem proving, any unifier will work — there is no reason to prefer the most general one. Why is using the MGU specifically important?
AThe MGU is always the most specific substitution and produces the most instantiated resolvent
BUsing the MGU keeps the resolvent as general as possible — unnecessary variable bindings in a more specific unifier restrict what subsequent inference steps can do with those variables
CThe MGU is required by Prolog syntax but has no logical significance
DMore specific unifiers are computationally harder to compute than the MGU
If you use a more specific unifier that binds extra variables unnecessarily, the resulting resolvent carries those commitments through the entire proof. Subsequent resolution steps that might need those variables to take different values are blocked. The MGU leaves the maximum freedom: it binds only what the current step requires, and all other variables remain available. This is not just efficiency — it is what makes the resolution proof system complete: using only MGUs guarantees you explore all possible inferences.
Question 3 True / False
The occurs check — verifying that variable x does not appear in term t before creating the binding x ↦ t — is merely an optimization that can safely be skipped in most practical theorem provers.
TTrue
FFalse
Answer: False
Skipping the occurs check can create unsound circular bindings. Without it, a unifier might bind x ↦ f(x), creating a circular term with no finite solution. An algorithm without the occurs check may loop forever trying to construct this infinite term, or produce a substitution that makes the unification 'succeed' with a non-terminating circular structure — leading to unsound inferences. Many Prolog implementations skip the occurs check for speed, which makes them technically unsound, but for a correct theorem prover the occurs check is required for soundness.
Question 4 True / False
For any two unifiable terms, the MGU is unique up to variable renaming — it is a canonical object determined by the terms themselves, not an arbitrary choice among unifiers.
TTrue
FFalse
Answer: True
This uniqueness is what makes the MGU well-defined as an algorithm output and why resolution is deterministic in its inference steps. If multiple MGUs existed that were genuinely different (not just renamings of each other), resolution would be non-deterministic in a way that could affect completeness. The uniqueness theorem guarantees that any correct unification algorithm will produce the same canonical answer (up to renaming), so the resolvent produced by a resolution step is unique regardless of which algorithm computed the MGU.
Question 5 Short Answer
In resolution-based theorem proving, why must the MGU substitution be applied to all literals in both clauses being resolved, not just to the specific literals that were matched?
Think about your answer, then reveal below.
Model answer: The MGU may bind variables that appear in other literals of the same clause, not just in the matched pair. Applying the substitution only to the matched literals would leave those other literals with the old variable names, creating an inconsistency: the same variable would have one value in the matched literal (already resolved away) and a different, unsubstituted form in the remaining literals. The resolvent must be logically coherent — all occurrences of each variable must be uniformly substituted — and as general as possible, which requires applying the MGU throughout both clauses.
For example, if clause 1 is P(x) ∨ Q(x) and clause 2 is ¬P(f(a)), the MGU for P(x) and P(f(a)) is {x ↦ f(a)}. The resolvent is Q(x) with the substitution applied: Q(f(a)). If we only applied the MGU to the P-literals and left Q(x) untouched, we'd have an unsubstituted x floating in the resolvent that was supposed to be bound to f(a) — an incoherent clause. Uniform application preserves the meaning of the variables across the clause.