Can someone explain the difference between the == and the = operator in Prolog? I know that X = Y means X unifies with Y and is true if X already unifies with Y or can be made to, but I don't understand how this differs from ==.
Follow up: That (see Accepted Answer) makes sense. One more question though, is there ever a situation where X \= Y is true and X \== Y is false (or vice-versa)? That is, does X \= Y test if they cannot be unified or if they are not currently unified?
The = "operator" in Prolog is actually a predicate (with infix notation) =/2 that succeeds when the two terms are unified. Thus X = 2 or 2 = X amount to the same thing, a goal to unify X with 2.
The == "operator" differs in that it succeeds only if the two terms are already identical without further unification. Thus X == 2 is true only if the variable X had previously been assigned the value 2.
Added: It's interesting to work through what happens when "not" gets mixed into these goals, per the comment by JohnS below. See the nice set of examples in the Amzi! Prolog documentation.
\= means the two terms cannot be unified, i.e. that unification fails. As with all applications of negation as failure, "not unified" does not (and cannot) result in any unification between terms.
\== means the two terms are not identical. Here also no unification takes place even if this succeeds.
Finally think about what not(not(X = Y)) will do. The inner goal succeeds if X and Y (which can be arbitrary terms) can be unified, and so will the double negation of that. However wrapping the inner goal inside the double negation produces a goal that succeeds if the two terms can be unified but without unifying those terms.
It is left as an exercise for the reader to contemplate whether not(not(X == Y)) has any similar utility.