Artificial Intelligence - foundations of computational agents -- 12.4 Proofs and Substitutions

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

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₁/t₁,...,V_n/t_n}, where each V_i is a distinct variable and each t_i is a term. The element V_i/t_i is a binding for variable V_i. A substitution is in normal form if no V_i appears in any 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₁/t₁,...,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_i in e replaced by the corresponding t_i. 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 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₁ and e₂ if e₁σ is identical to e₂σ. 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 e₁ and e₂ if

σ is a unifier of the two expressions, and
if another substitution σ' exists that is also a unifier of e₁ and e₂, then eσ' must be an instance of e σ for all expressions e.

Expression e₁ is a renaming of e₂ 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 e₁ and e₂, then e₁σ is a renaming of e₁σ'.

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.