subsumes_chk/2 meta-logicalsubsumes_chk(+General, +Specific)
True when General subsumes Specific; that is, when Specific is an instance of General.
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.
library(subsumes), library(occurs)