Resolution with unification

• May 29th 2011, 12:05 PM
Keep
Resolution with unification
I have this formula and I need to resolve it with unification:

{ ¬ P1(h(x)), P2(g(y))} , {P1(z), P2(z), P1(h(y)), P3(g(y)) }

I have used this as a unificator:

$\sigma = z/h(v), x/v, y/v$

and I got { $P2(g(v)), P2(h(v)), P3(g(v))}$

However if I use the unificator:

$\sigma = z/g(v), x/v, y/v$

I get { P2(g(v))} , {P1(g(v)), P3(g(v)) }

so are both ways right or only one is right? In which case, which one is it then?
• May 29th 2011, 03:18 PM
emakarov
Both ways are right, though in both cases you don't use the most general unifiers (MGU). If you cancel the first literals of each disjunct, the MGU is z/h(x) and the resulting disjunct is

{P2(g(y)), P2(h(x)), P1(h(y)), P3(g(y))}

If you match ¬P1(h(x)) with P1(h(y)), the MGU is x/y and the result is

{P2(g(y)), P1(z), P2(z), P3(g(y))}

Edit: changed the MGU from x/h(x) to z/h(x).
• May 29th 2011, 03:21 PM
Keep
Thanks. So both ways are right. Is there on way which is considered "better" then? Me, the second one looks a little bit nicer to me :-) { P2(g(v))} , {P1(g(v)), P3(g(v)) }

And oh I really don't what MGUs are.
• May 29th 2011, 03:50 PM
emakarov
I don't know any sense in which one of your results is better than the other. However, if you use unifiers that are not most general, then you may not be able to obtain an empty disjunct even though the original set of disjuncts is contradictory, i.e., then resolution would cease to be a complete inference rule.

A substitution θ is more general than σ if there is another substitution η such that σ = θη, i.e., η further specializes θ to obtain σ. For example, [z/h(x)] is more general than [z/h(v), x/v, y/v] because [z/h(v), x/v, y/v] = [z/h(x)][x/v,y/v]. In other words, resolution only requires replacing z with h(x); it does not force you to replace both x and y with v.
• May 29th 2011, 04:11 PM
Keep
Yeah I understood it now. Thank you so much!