13.4 Proofs and Substitutions

13.4.1 Instances and Substitutions

An instance of a clause is obtained by uniformly substituting terms for variables in the clause. All occurrences of a particular variable are replaced by the same term.

The specification of which value is assigned to each variable is called a substitution. A substitution is a set of the form {V1/t1,,Vn/tn}, where each Vi is a distinct variable and each ti is a term. The element Vi/ti is a binding for variable Vi. A substitution is in normal form if no Vi appears in any tj.

Example 13.14.

For example, {X/Y,Z/a} is a substitution in normal form that binds X to Y and binds Z to a. The substitution{X/Y,Z/X} is not in normal form, because the variable X occurs both on the left and on the right of a binding.

The application of a substitution σ={V1/t1,,Vn/tn} to expression e, written eσ, is an expression that is the same as the original expression e except that each occurrence of Vi in e is replaced by the corresponding ti. The expression eσ is called an instance of e. If eσ does not contain any variables, it is called a ground instance of e.

Example 13.15.

Some applications of substitutions are


Substitutions can apply to clauses, atoms, and terms. For example, the result of applying the substitution {X/Y,Z/a} to the clause


is the clause


A substitution σ is a unifier of expressions e1 and e2 if e1σ is identical to e2σ. That is, a unifier of two expressions is a substitution that when applied to each expression results in the same expression.

Example 13.16.

{X/a,Y/b} is a unifier of t(a,Y,c) and t(X,b,c) as


Expressions can have many unifiers.

Example 13.17.

Atoms p(X,Y) and p(Z,Z) have many unifiers, including {X/b,Y/b,Z/b}, {X/c,Y/c,Z/c}, {X/Z,Y/Z} and {Y/X,Z/X}. The last two unifiers are more general than the first two, because the first two both have X the same as Z and Y the same as Z but make more commitments to what these values are.

Substitution σ is a most general unifier (MGU) of expressions e1 and e2 if

  • σ is a unifier of the two expressions, and

  • if substitution σ is also a unifier of e1 and e2, then eσ must be an instance of eσ for all expressions e.

Expression e1 is a renaming of e2 if they differ only in the names of variables. In this case, they are both instances of each other.

If two expressions have a unifier, they have at least one MGU. The expressions resulting from applying the MGUs to the expressions are all renamings of each other. That is, if σ and σ are both MGUs of expressions e1 and e2, then e1σ is a renaming of e1σ.

Example 13.18.

{X/Z,Y/Z} and {Z/X,Y/X} are both MGUs of p(X,Y) and p(Z,Z). The resulting applications


are renamings of each other.