Results 1 to 5 of 5

Math Help - Resolution with unification

  1. #1
    Member
    Joined
    Mar 2009
    Posts
    77

    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?
    Last edited by Keep; May 29th 2011 at 12:16 PM.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,417
    Thanks
    718
    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).
    Last edited by emakarov; May 29th 2011 at 03:47 PM.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Member
    Joined
    Mar 2009
    Posts
    77
    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.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,417
    Thanks
    718
    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.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Member
    Joined
    Mar 2009
    Posts
    77
    Yeah I understood it now. Thank you so much!
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Resolution
    Posted in the Math Topics Forum
    Replies: 0
    Last Post: November 6th 2011, 06:14 PM
  2. Help with resolution principle, please
    Posted in the Discrete Math Forum
    Replies: 0
    Last Post: February 3rd 2010, 01:49 PM
  3. resolution of vectors
    Posted in the Math Topics Forum
    Replies: 0
    Last Post: September 20th 2009, 04:34 PM
  4. Equation without resolution in R
    Posted in the Trigonometry Forum
    Replies: 1
    Last Post: June 16th 2009, 11:53 AM
  5. Unique resolution
    Posted in the Pre-Calculus Forum
    Replies: 2
    Last Post: June 6th 2009, 02:42 AM

Search Tags


/mathhelpforum @mathhelpforum