Unification

Before we define the concept of a unifier we must extend the book's concept of substitution. A substitution can now be a set of pairs of variables and their replacements, written

$$[t_1/x_1, t_2/x_2, \ldots, t_n/x_n].$$

Applying a substitution to an expression (either a term or formula) means to simulatenously replace each variable ($x_i$) with its corresponding term ($t_i$).

A substitution can never contain a pair of the form $x/x$.

For example, if we have $\theta = [y/x, f(x)/y, c/z]$, the results of applying $\theta$ to the term $P(x,y,z,w)$ ( $\theta(P(x,y,z,w))$) is $P(y,f(x),c,w)$.