Thread: Resolution with unification

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

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.

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.

Yeah I understood it now. Thank you so much!