Unify terms

Unification is the core operation that occurs during Prolog execution. Most unification is performed as goals unify with heads of clauses. However, it is often useful to invoke unification explicitly, or to check whether two terms cannot successfully unify. These predicates should not be confused with the '=='/2, '\=='/2 and eq/2 predicates that are described in the Classify, compare, and sort terms section.

Explicit unification is performed by:

X = Y

This goal succeeds if and only if X and Y unify. In subsequent goals, X and Y are unified.

Unification is of course at the heart of Prolog. The '='/2 predicate and operator definition is equivalent to:

:- op(700, xfy, '=').
'='(X, X).

An explicit check that two terms cannot unify is performed by:

X \= Y

This goal succeeds if X and Y cannot be unified. In subsequent goals, X and Y are not unified.

The '\='/2 predicate and operator definition is equivalent to:

:- op(700, xfx, '\=').
'\='(X, X) :- !, fail.
'\='(_, _).