A term generalizing that of pattern-matching that is the logic programming equivalent of instantiation in logic.

Citing from FOLDOC (slightly reformatted, see below):

When two terms are to be unified, they are compared: The result of unification is either failure or success with a set of variable bindings, known as a "unifier". There may be many such unifiers for any pair of terms but there will be at most one "Most General Unifier" (MGU), other unifiers simply add extra bindings for sub-terms which are variables in the original terms.

This page is linked from: Alan Bundy   Dispatch   LIFE   TXL