Unification Problem

A unification problem $\mathcal{U}$ is a set of equations between terms containing variables.

$$\{s_1=t_1,\dots ,t_n=t_n\}$$

A solution to $\mathcal{U}$, also called a unifier, is a substitution $\sigma$, such that when applied to every term in $\mathcal{U}$, for each equation $s_i=t_i$, the terms $s_i\sigma$ and $t_i\sigma$ are syntactically identical.