What is \= in Swi-Prolog

Question

As I browse through the internet to find information about Swi-prolog, I happened to find \= , with given example like X \= Y. Can someone tell me what it is? Is it some kind of arithmetic operation?

Answer 1

This is a basic operator from Prolog, not specific to SWI-Prolog.

It means the left-hand-side term and the right-hand-side term do not unify (now and thus also in any future instantiation down this path of the search tree), so it is a question about the structure of those terms. You could also write \+ (LHS = RHS) instead of LHS \= RHS.

These do not unify:

?- a \= b.
true.

?- f(X) \= g(Y).
true.

But these do, so the answer is false:

?- f(X) \= f(Y).
false.

Instantiate on the right, still unify:

?- f(X) \= f(a).
false.

Instantiate on the left, unification is now impossible:

?- f(b) \= f(a).
true.

It may be interesting to use dif/2 (dif(X,Y): "ensure X and Y wont' unify down this path", which sets up a constraint involving its arguments that vetoes (and fails) any attempt to make X and Y the same.

After this, X and Y shall not unify. The residual constraint is printed:

?- dif(X,Y).
dif(X,Y).

Trying to unify X and Y after dif/2 fails:

?- dif(X,Y),X=Y.
false.

Refining X to 1 is still possible:

?- dif(X,Y),X=1.
X = 1,
dif(1,Y).

Refining X to 1 and Y to 2 is certainly possible:

?- dif(X,Y),X=1,Y=2.
X = 1,
Y = 2.

Refining both to 1 is not possible:

?- dif(X,Y),X=1,Y=1.
false.