Most General Unifier computation

Question

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?

Doug Spoonwood · Answer

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.

With your example:

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)).

One Answer