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?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.