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

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

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

are renamings of each other.