The predicates of this section implement weak unification and syntantic unification.

Weak unification.

'~'( @term, @term )

X ~ Y is true if and only if X and Y are weakly unifiable. True if the weak unification succeeds.

Unification.

'='( @term, @term )

X = Y is true if and only if X and Y are unifiable. True if the unification succeeds.

Not weak unification.

'\~'( @term, @term )

X \~ Y is true if and only if X and Y are not weakly unifiable.

Not unification.

'\='( @term, @term )

X \= Y is true if and only if X and Y are not unifiable.

Weak unification with occurs check.

weakly_unify_with_occurs_check( @term, @term )

weakly_unify_with_occurs_check(X, Y) is true if and only if X and Y are weakly unifiable. True if the weak unification succeeds.

Unification with occurs check.

unify_with_occurs_check( @term, @term )

unify_with_occurs_check(X, Y) is true if and only if X and Y are unifiable. True if the unification succeeds.