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 inXandYin 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 `?=(`

holds:
`X`,`Y`)

?-dif(X,Y).

The goal:

?-subsumes_term(General,Specific).

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

Send feedback on this subject.