Introduction to Logic

Exercise 12.2 - Unification

For each of the following pairs of expressions, say which substitution, if any, is a most general unifier.

1.p(x,x) and p(a,y) 
  {xa} 
  {ya} 
  {xa, ya} 
  Not unifiable 
 
2.p(x,x) and p(f(y),z) 
  {xf(a), ya, zf(a)} 
  {xf(y), zf(y)} 
  {xf(y)} 
  Not unifiable 
 
3.p(x,x) and p(f(y),y) 
  {xf(a), ya} 
  {xf(y), yf(y)} 
  {xf(y)} 
  Not unifiable 
 
4.p(f(x,y),g(z,z)) and p(f(f(w,z),v),w) 
  {xw, yz, wg(z,z)} 
  {xf(f(w,z),v), yv, wg(z,z)} 
  {xf(g(z,z),z), yv, wg(z,z)} 
  Not unifiable