Exercise Chapter 4.1 on Unification

1. 2+1=3 fails.

   We can tell immediately that 3 is an atom but what about 2+1? This does not look like an atom ---indeed it is not. The only way that 2+1=3 is if Prolog were to automatically try to evaluate any `sum' it finds before trying to do the unification. Prolog does not do this.

2. f(X,a)=f(a,X) succeeds with X=a.

   Here, the predicates are the same (so far so good). Now we match the first arguments: they can be made the same if X=a (so far so good). Now we look at the second argument: does a match with X? yes.

3. fred=fred succeeds.

4. likes(jane,X)=likes(X,jim) fails.

   Here, the predicates are the same (so far so good). Now we match the first arguments: they can be made the same if X=jane (so far so good). Now we look at the second argument: does X match with jim? Well, X is bound to jane and jane does not match with jim. So the unification fails.

5. f(X,Y)=f(P,P) succeeds with X=Y=P.

   Here, the predicates are the same. Now we match the first arguments: they can be made the same if X=P. Now we look at the second argument: does Y match with P? yes, and since X=P we get our final result.