The concept of unification comes from first-order logic: given two terms s and t, to unify them means to find a substitution σ over their free variables such that sσ = tσ. A substitution unifying two terms is called a unifier for them.
The other central component of how a Prolog program runs is resolution. Resolution is an inference rule such that, given two clauses (i.e., disjunctions) containing complementary unifiable literals (i.e., an atom or its negation), produces a new clause by taking the literals of the two clauses, except for the complementary ones, and applying the unifier on them.
