I have the following first order logic expressions:

$f(g(a, h(b)), g(x, y)),~f(g(z,y), g(y, y))$

and I want to compute the most general unifier for them. If I follow the algorithm found on these slides then I get the following.

\begin{align*} S_0 &= \{f(g(a, h(b)), g(x, y)), f(g(z,y), g(y, y))\}\\ D_0 &= \{g(a, h(b)),g(z,y)\} &[\text{first disagreement set}]\\ &\text{(need to unify these two functions)}\\ D_0'&= \{a,z\} &[\text{first sub-disagreement set}]\\ \sigma &= \{z=a\}\\ D_0''&=\{h(b),y\} &[\text{second sub-disagreement set}]\\ \sigma &= \{z=a, y=h(b)\}\\ S_1 &= \{f(g(a, h(b)), g(x, h(b))), f(g(a,h(b)), g(h(b), h(b)))\}\\ D_0 &= \{x,h(b)\} &[\text{second disagreement set}]\\ \sigma &= \{z=a,y=h(b),x=h(b)\}\\ S_2 &= \{f(g(a, h(b)), g(h(b), h(b))), f(g(a,h(b)), g(h(b), h(b)))\} \end{align*} No disagreement, unifier found! $\sigma = \{z=a,y=h(b),x=h(b)\}$.

However, this is not the most general unifier as we have $\{y=h(b),x=h(b)\}\in \sigma$, so i think the MGU should actually be $\sigma' = \{z=a,y=h(b),x=y\}$.

Is this correct? When I use Prolog to unify them, it gives $\sigma'$. What did I do wrong in my following of the algorithm, so that it gave me a unifier that wasn't the most general?


1 Answer 1


There seems to be a small confusion with the notation. Notice that $\sigma = \{z = a, \ y = h(b), \ x = h(b) \}$ and $\sigma' = \{z = a, \ y = h(b), \ x = y \}$ are the same unifier, written in a different way. It doesn't matter if we write $x = y$ or $x = h(b)$, since we also have $y = h(b)$. Hence, you did nothing wrong and you have computed the most general unifier.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.