subsumes_chk/2 meta-logical


subsumes_chk(+General, +Specific)

True when General subsumes Specific; that is, when Specific is an instance of General.


General term

Specific term


In previous releases, subsumes_chk/2 was available as a library predicate. In release 2.5, it was made part of the system because it was found to be useful in applications such as writing theorem provers. The built-in predicate behaves identically to the original version of subsumes_chk/2 but is much more efficient.

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.


There are two other related predicates defined in library(subsumes), subsumes/2 and variant/2. These predicates are defined in terms of subsumes_chk/2, and they are still available in that library package.

See Also

library(subsumes), library(occurs)