1
$\begingroup$

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?

$\endgroup$

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.