FASILL documentation Predicate Reference term unification

Term unification

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

'~'/2

Weak unification.

'~'( @term, @term )

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

'='/2

Unification.

'='( @term, @term )

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

'\~'/2

Not weak unification.

'\~'( @term, @term )

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

'\='/2

Not unification.

'\='( @term, @term )

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

weakly_unify_with_occurs_check/2

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.

unify_with_occurs_check/2

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.