## 12.4 Proofs and Substitutions

Both the bottom-up and top-down propositional proof procedures of Section 5.2.2 can be extended to Datalog.

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 proof procedure extended for
variables must account for the fact that a free variable in a clause
means that any instance of the clause is *true*. A proof
may have to use different instances of the same clause in a single proof.
The specification of what value is assigned to each variable is called
a substitution.

A **substitution** is a finite set of
the form *{V _{1}/t_{1},...,V_{n}/t_{n}}*, where each

*V*is a distinct variable and each

_{i}*t*is a term. The element

_{i}*V*is a

_{i}/t_{i}**binding**for variable

*V*. A substitution is in

_{i}**normal form**if no

*V*appears in any

_{i}*t*.

_{j}**Example 12.13:**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 *σ={V _{1}/t_{1},...,V_{n}/t_{n}}* to expression

*e*, written

*eσ*, is an expression that is like the original expression

*e*but with every occurrence of

*V*in

_{i}*e*replaced by the corresponding

*t*. The expression

_{i}*eσ*is called an

**instance**of

*e*. If

*eσ*does not contain any variables, it is called a

**ground instance**of

*e*.

**Example 12.14:**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 *e _{1}* and

*e*if

_{2}*e*is identical to

_{1}σ*e*. That is, a unifier of two expressions is a substitution that when applied to each expression results in the same expression.

_{2}σ**Example 12.15:**

*{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 12.16:**Atoms

*p(X,Y)*and

*p(Z,Z)*have many unifiers, including

*{X/b,Y/b,Z/b}*,

*{X/c,Y/c,Y/c}*, and

*{X/Z,Y/Z}*. The third unifier is 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 in what these values are.

Substitution *σ* is a **most general unifier** (**MGU**) of
expressions *e _{1}* and

*e*if

_{2}*σ*is a unifier of the two expressions, and- if another
substitution
*σ'*exists that is also a unifier of*e*and_{1}*e*, then_{2}*eσ'*must be an instance of*e σ*for all expressions*e*.

Expression *e _{1}* is a

**renaming**of

*e*if they differ only in the names of variables. In this case, they are both instances of each other.

_{2}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 *e _{1}* and

*e*, then

_{2}*e*is a renaming of

_{1}σ*e*.

_{1}σ'**Example 12.17:**

*{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.