Prolog matches male(X) with male(jan), thereby instantiating the variable X to jan.

There are three types of terms:

1. Constants. These can either be atoms (such as jan) or numbers (such as 24).
2. Variables.
3. Complex terms. These have the form: functor(term_1,...,term_n).

    Two terms match, if they are equal or if they contain variables that can be instantiated
    in such a way that the resulting terms are equal.

Usually we also want to know in what way the variables have to be instantiated to make them equal. When Prolog matches two terms it performs all the necessary instantiations, so that the terms really are equal afterwards. This functionality together with the fact that we are allowed to build complex terms (that is, recursively structured terms) makes matching a quite powerful mechanism. Matching is one of the fundamental ideas in Prolog.

1. If t1 and t2 are constants, then t1 and t2 match if and only if they are the same atom, or the same number.
2. If t1 is a variable and t2 is any type of term, then t1 and t2 match, and t1 is instantiated to t2.
3. If t1 and t2 are complex terms, then they match if and only if:
   1. They have the same functor and arity.
   2. All their corresponding arguments match
   3. The variable instantiations are compatible  (it is not possible to instantiate variable X to jan, when matching one pair of arguments, and to then instantiate X to eva, when matching another pair of arguments.)
4. Two terms match if and only if it follows from the previous three clauses that they match.