the algorithm (shown in No description for this link) takes two sentences and returns a unifier for them (a substitution) if one exists: let us look at some examples of how should behave. suppose we have a query : whom does John know? answers to this query can be found by finding all sentences in the knowledge base that unify with . here are the results of unification with four different sentences that might be in the knowledge base:
the last unification fails because
cannot take on the values John and Elizabeth at the same time. now, remember that
means "everyone knows Elizabeth", so we should be able to infer that John knows Elizabeth. the problem arises only because the two sentences happen to use the same variable name,
. the problem can be avoided by standardizing apart one of the two sentences being unified, which means renaming its variables to avoid name clashes. for example, we can rename
in
to
(a new variable name) without changing its meaning. now the unification will work:
there is one more complication: we said that should return a substitution that makes the two arguments look the same. but there could be more than one such unifier.
for example, could return or could return . the first unifier gives as the result of unification, whereas the second gives . the second result could be obtained from the first by an additional substitution ; we say that the first unifier is more general than the second, because it places fewer restrictions on the values of the variables.
every unifiable pair of expressions has a single most general unifier (MGU) that is unique up to renaming and substitution of variables. for example, and are considered equivalent, as are and .
an algorithm for computing most general unifiers is shown in No description for this link. the process is simple: recursively explore the two expressions simultaneously "side by side", building up a unifier along the way, but failing if two corresponding points in the structures do not match. there is one expensive step: when matching a variable against a complex term, one must check whether the variable itself occurs inside the term; if it does, the match fails because no consistent unifier can be constructed. for example, cant unify with . this so-called occur check makes the complexity of the entire algorithm quadratic in the size of the expressions being unified. some systems, including many logic programming systems, simply omit the occur check and put the onus on the user to avoid making unsound inferences as a result. other systems use more complex unification algorithms with linear time complexity.
the unification algorithm. the arguments and can be any expression: a constant or variable, or a compound expression such as a complex sentence or term, or a list of expressions. the argument is a substitution, initially the empty substitution, but with pairs added to it as we recurse through the inputs, comparing the expressions element by element. in a compound expression such as field picks out the function symbol and field picks out the argument list .