# Most General Unifier computation

Mathematics Asked by Milano on February 16, 2021

I’m trying to compute a most general unifier. There are many rules and I’m confused by them.

So here is the example:

{P(z,g(c)),P(g(x),z),P(z,z),P(g(y),g(c))} – x, y and z are variables an c is a constant

I know that I can’t substitute constant by variable.

Could you give me a hint how to compute that? Those rules I have to know to be able to solve this kind of examples please?

I think that MGU is {z/g(c),x/y,y/c} is it True?

The most general unifier should reduce all predicates P(),X(),Z() to one? So there is just one predicate?

You can compute most general unifiers by taking formulas pairwise and lining them up to help you to compute most general unifiers for the pairs.

P(z,   g(c))
|    ----
----  |
P(g(x), z)


Thus, z/g(x) yields P(g(x), g(c)) and P(g(x), g(x)). Consequently,

z/g(x), x/c which becomes {z/g(c), x/c} indicates the most general unifier of those two wffs. Thus, both formulas unify to P(g(c), g(c)).

P(z, z) only has z in it, and we already have z/g(c). Thus, P(z, z) and P(g(c), g(c)) unify to P(g(c), g(c)) with most general unifier z/g(c).

P(g(y), g(c)) and P(g(c), g(c)) unify to P(g(c), g(c)) with most general unifier y/c.

Putting all the substitutions together we have

{z/g(c), x/c, y/c} as the most general unifier of all the wffs above.

And thus if you use the most general unifier {z/g(c), x/c, y/c} on all the predicate in

{P(z,g(c)),P(g(x),z),P(z,z),P(g(y),g(c))}

after substitution they all have the form P(g(c), g(c)).

Answered by Doug Spoonwood on February 16, 2021