4.8.1.2 Unification

The following predicates are related to unification. Unless mentioned otherwise, unification is performed without occurs check (see ref-sem-occ).

To unify two terms, simply use:

?- X = Y.

Please note:

• Do Not confuse this predicate with =:=/2 (arithmetic comparison) or ==/2 (term identity).
• =/2 binds free variables in X and Y in order to make them identical.

To unify two terms with occurs check, use:

?- unify_with_occurs_check(X,Y).

To check whether two terms do not unify, use the following, which is equivalent to \+ (X=Y):

?- X \= Y.

To check whether two terms are either strictly identical or do not unify, use the following. This construct is useful in the context of when/2:

?- ?=(X,Y).

To constrain two terms to not unify, use the following. It blocks until ?=(X,Y) holds:

?- dif(X,Y).

The goal:

?- subsumes_term(General,Specific).

is true when Specific is an instance of General. It does not bind any variables.