Unification is the name given to the way Prolog does its matching. We will not do more than sketch the basic ideas here. Basically, an attempt can be made to unify any pair of valid Prolog entities or terms.
Unification is more than simple matching. A naive view of the matching process might be represented by the question ``can the target object be made to fit one of the source objects''. The implicit assumption is that the source is not affected ---only the target is coerced to make it look like some source object.
Unification implies mutual coercion. There is an attempt to alter both the target and the current source object to make them look the same.
Consider how we might match the term book(waverley,X) against some clause for which book(Y, scott) is the head. The naive approach might be that X/scott is the correct substitution ---or even that the matching cannot be done. Unification provides the substitutions X/scott and Y/waverley. With these substitutions both terms look like book(waverley,scott).
The substitution X/scott and Y/waverley is known as a unifier ---to be precise, the most general unifier. If we unify X with Y then one unifier might be the substitution X/1 and Y/1 but this is not the most general unifier.
Consider the infix predicate =/2.
Certain `built-in' Prolog predicates are provided that can be written in a special infix or prefix form (there are no postfix ones provided ---that is not because they could not be!) For example, 1=2 is written as =(1,2) in standard Prolog form.
Prolog tries to unify both the arguments of this predicate. Here are some possible unifications:
It is worth making a distinction here between the textual name of a logical variable and its run-time name. Consider a query likes(jim,X). Suppose there is one clause: likes(X,fred) ---this has the reading that ``everyone likes fred'' and mentions a variable with the textual name of X. The query also mentions a specific variable by the textual name of X. By the scope rule for variables, we know that these two variables, although textually the same, are really different. So now consider whether the head of the clause likes(X,fred) unifies with the current goal likes(jim,X).
We might then reason like this: the task is to decide whether or not likes(jim,X)=likes(X,fred) succeeds. If this is so then, matching the first arguments, we get X=jim. Then we try to match the second arguments. Now can X=fred? If X=jim then the answer is no. How is this? The answer we expect (logically) is that ``jim likes fred''. We really ought to distinguish every variable mentioned from each other according to the scope rules. This means that the query is better thought of as, say, likes(jim,X and the clause is then likes(X,fred). In the literature the process of making sure that variables with the same textual name but in different scopes are really different is known as standardisation apart!