## 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 {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 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 σ={V1/t1,...,Vn/tn} to expression e, written , is an expression that is like the original expression e but with every occurrence of Vi in e replaced by the corresponding ti. The expression is called an instance of e. If 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 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 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 e1 and e2 if

• σ is a unifier of the two expressions, and
• if another substitution σ' exists that 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 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.