#### 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.
```

• 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.

Send feedback on this subject.