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.
- Don’t confuse this predicate with
=:=/2(arithmetic comparison) or
=/2binds free variables in X and Y in order to make them identical.
To unify two terms with occurs-check, use:
To check whether two terms don’t unify, use the following, which is
?- X \= Y.
To check whether two terms are either strictly identical or don’t
unify, use the following. This construct is useful in the context of
To constrain two terms to not unify, use the following. It blocks
is true when Specific is an instance of General. It does not bind any variables.