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?
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.