foundations of computational agents
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 , where each is a distinct variable and each is a term. The element is a binding for variable . A substitution is in normal form if no appears in any .
For example, is a substitution in normal form that binds to and binds to . The substitution is not in normal form, because the variable occurs both on the left and on the right of a binding.
The application of a substitution to expression , written , is an expression that is the same as the original expression except that each occurrence of in is replaced by the corresponding . The expression is called an instance of . If does not contain any variables, it is called a ground instance of .
Some applications of substitutions are
Substitutions can apply to clauses, atoms, and terms. For example, the result of applying the substitution to the clause
is the clause
A substitution is a unifier of expressions and if is identical to . That is, a unifier of two expressions is a substitution that when applied to each expression results in the same expression.
is a unifier of and as
Expressions can have many unifiers.
Atoms and have many unifiers, including , , and . The last two unifiers are more general than the first two, because the first two both have the same as and the same as but make more commitments to what these values are.
Substitution is a most general unifier (MGU) of expressions and if
is a unifier of the two expressions, and
if substitution is also a unifier of and , then must be an instance of for all expressions .
Expression is a renaming of 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 and , then is a renaming of .
and are both MGUs of and . The resulting applications
are renamings of each other.