Contents    Page-10    Prev    Next    Page+10    Index   

Examples of Unification

Consider unifying the literal P(x, g(x)) with:

  1. P(z,y) : unifies with {x/z, g(x)/y}
  2. P(z, g(z)): unifies with {x/z} or {z/x}
  3. P(Socrates, g(Socrates)) : unifies, {Socrates/x}
  4. P(z, g(y)): unifies with {x/z, x/y} or {z/x, z/y}
  5. P(g(y), z): unifies with {g(y)/x, g(g(y))/z}
  6. P(Socrates, f(Socrates)) : does not unify: f and g do not match.
  7. P(g(y), y) : does not unify: no substitution works.