\begin{frame} \small \begin{definition}[Unification Problem] \smallskip \begin{tabular}{ll@{\qquad\qquad}ll} instance: & terms $s$, $t$ \\[.5ex] question: & $\exists$ $\underbrace{\mathstrut\text{substitution $\sigma$}}_% {\makebox[0mm][c]{\alert<1>{unifier}}}\colon ~ s\sigma = t\sigma$ ? \end{tabular} \end{definition} \smallskip \begin{definition}<2-> \smallskip substitution $\sigma$ is \alert<2>{at least as general} as $\tau$ ($\alert<2>{\sigma \subsumes \tau}$) if $\exists$ substitution $\rho\colon \sigma\rho = \tau$ \smallskip \end{definition} \smallskip \begin{lemma}<3-> \smallskip $\prinstance$ is well-founded order on substitutions (with a finite domain) \smallskip \end{lemma} \smallskip \begin{definition}<4-> \smallskip \alert<4>{most general} unifier (\alert<4>{mgu}) is at least as general as any other unifier \end{definition} \end{frame}