\begin{frame} \small \begin{definition}[Common Instance] \smallskip \begin{tabular}{ll@{\qquad\qquad}ll} instance: & terms $s$, $t$ \\[.5ex] question: & $\exists$ $\mathstrut\text{substitutions $\sigma$, $\tau$}\colon ~ s\sigma = t\tau$ ? \end{tabular} \end{definition} \pause\medskip \begin{definition} \alert{most general} common instance (\alert{mgci}) is at least as general as any other common instance \end{definition} \pause\medskip We can compute the most general common instance as follows: \begin{itemize} \pause \item let $\gamma$ be a renaming of the variables in $t$\\ such that $s$ and $t\gamma$ have no variables in common \pause \item if $\rho$ is the mgu for $s$ and $t\gamma$, then $s\rho = t\gamma\rho$ is the mgci for $s$ and $t$ % \pause % \item if $\sigma$ exists, then $s\sigma = t (\gamma\sigma)$ is the mgci\\ % (with substitutions $\sigma$ and $\gamma\sigma$, respectively) \end{itemize} \end{frame}