13.4 Proofs and Substitutions

The third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including full text).

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

p⁢(a,X)⁢{X/c}=p⁢(a,c).
p⁢(Y,c)⁢{Y/a}=p⁢(a,c).
p⁢(a,X)⁢{Y/a,Z/X}=p⁢(a,X).
p⁢(X,X,Y,Y,Z)⁢{X/Z,Y/t}=p⁢(Z,Z,t,t,Z).

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

p⁢(X,Y)←⁢q⁢(a,Z,X,Y,Z)

is the clause

p⁢(Y,Y)←⁢q⁢(a,a,Y,Y,a).

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

t⁢(a,Y,c)⁢{X/a,Y/b}=t⁢(X,b,c)⁢{X/a,Y/b}=t⁢(a,b,c).

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

p⁢(X,Y)⁢{X/Z,Y/Z}=p⁢(Z,Z)
p⁢(X,Y)⁢{Z/X,Y/X}=p⁢(X,X)

are renamings of each other.