If X
cannot be matched with Y
the goal succeeds else the goal fails. A X\==Y
goal will only consider an uninstantiated variable to be equal to another uninstantiated variable that is already sharing with it.
Examples
?- X \== Y.
X = UNINSTANTIATED VARIABLE
Y = UNINSTANTIATED VARIABLE
yes
?- X \== X.
no
?- X=Y, X \== Y, Y=1.
no
?- X \== Y, Y = 1, X = Y.
X = 1
Y = 1
yes
?- append([A|B],C) \== append(X,Y).
A = UNINSTANTIATED VARIABLE
B = UNINSTANTIATED VARIABLE
C = UNINSTANTIATED VARIABLE
X = UNINSTANTIATED VARIABLE
Y = UNINSTANTIATED VARIABLE
yes
?- append([A|B],C) \== append([A|B],C).
no