Unification and Subsumption

To unify two items simply use =/2, which is defined as if by the clause

     =(X, X).

Please note: Do not confuse this predicate with =:=/2 (arithmetic comparison) or ==/2 (term identity).

Term subsumption is a sort of one-way unification. Term S and T unify if they have a common instance, and unification in Prolog instantiates both terms to that common instance. S subsumes T if T is already an instance of S. For our purposes, T is an instance of S if there is a substitution that leaves T unchanged and makes S identical to T.

Subsumption is checked by subsumes_chk/2. It is especially useful in applications such as theorem provers. The built-in predicate behaves identically to the original library version but is much more efficient.

Related predicates are defined in library(subsumes) and library(occurs). (For information on these packages see lib).