Term subsumption is a sort of one-way unification. Recall that terms S and T unify if they have a common instance, and that 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.
Two terms are alphabetic variants if they are identical except for variable names, and all common variables appear in corresponding positions. For example,
f(X,Z,X)are alphabetic variants;
This file used to define
subsumes_chk/2, but this is now a built-in
There are currently two predicates in this file:
)holds precisely when