Prolog unification
When programming in Prolog, we spend a lot of time thinking about how variables and rules “match” or “are assigned.” There are actually two aspects to this. The first, “unification,” regards how terms are matched and variables assigned to make terms match. The second, “resolution,” is described in separate notes. Resolution is only used if rules are involved. You may notice in these notes that no rules are involved since we are only talking about unification.
Prolog ‘Terms’
Prolog has three kinds of terms:

Constants like
42
(numbers) andfranklin
(atoms, i.e., lowercase words). 
Variables like
X
andPerson
(words that start with uppercase). 
Complex terms like
parent(franklin, bo)
andbaz(X, quux(Y))
.
Two terms unify if they can be matched. Two terms can be matched if:

they are the same term (obviously), or

they contain variables that can be uniformly instantiated so that the two terms without variables are the same. “Uniformly” instantiated means that each distinct variable gets the same value, e.g., all
X
variables in the term get the same value.
For example, suppose our knowledge base is:
woman(mia).
loves(vincent, angela).
loves(franklin, mia).

mia
andmia
unify because they are the same. 
mia
andX
unify becauseX
can be given the valuemia
so that the two terms (without variables) are the same. 
woman(mia)
andwoman(X)
unify becauseX
can be set tomia
which results in identical terms. 
loves(X, mia)
andloves(vincent, X)
cannot unify because there is no assignment forX
(given our knowledge base) that makes the two terms identical. 
loves(X, mia)
andloves(franklin, X)
also cannot unify (can you see why?).
We saw in the Prolog notes that we can “query”
the knowledge base and get, say, all the people who love mia
. When
we query with loves(X, mia).
we are asking Prolog to give us all the
values for X
that unify. These values are, essentially, the people
who love mia
.
A more formal definition
term1
and term2
unify whenever:

If
term1
andterm2
are constants, thenterm1
andterm2
unify if and only if they are the same atom, or the same number. 
If
term1
is a variable andterm2
is any type of term, thenterm1
andterm2
unify, andterm1
is instantiated toterm2
. (And vice versa.) (If they are both variables, they’re both instantiated to each other, and we say that they share values.) 
If
term1
andterm2
are complex terms, they unify if and only if:a. They have the same functor and arity. The functor is the “function” name (this functor is
foo
:foo(X, bar)
). The arity is the number of arguments for the functor (the arity forfoo(X, bar)
is 2).b. All of their corresponding arguments unify. Recursion!
c. The variable instantiations are compatible (i.e., the same variable is not given two different unifications/values).

Two terms unify if and only if they unify for one of the above three reasons (there are no reasons left unstated).
Practice
We’ll use the =
predicate to test if two terms unify. Prolog will
answer “Yes” if they do, as well as any sufficient variable
assignments to make the unification work.
Do these two terms unify?
? mia = mia.
Yes, from rule 1.
Do these two terms unify?
? mia = X.
Yes, from rule 2.
Do these two terms unify?
? X = Y.
Yes, from rule 2.
Do these two terms unify?
? k(s(g), Y) = k(X, t(k)).
Yes, from rule 3 and, in the recursion, from rule 2 in two cases (X
set to s(g)
and Y
set to t(k)
).
Do these two terms unify?
? k(s(g), Y) = k(s(g, X), Y).
No, because rule 3 fails in the recursion (in which rule 3 is invoked
again, and the arity of s(g)
does not match s(g, X)
).
Much of these notes were adapted from Learn Prolog Now!, a free online textbook.