library(subsumes)
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,Y,X)
andf(X,Z,X)
are alphabetic variants;f(X,Y,X)
andf(Y,X,Y)
are not;f(X,Y,X)
andf(X,Y,Y)
are not;f(X,Y,X)
andf(Z,V,Z)
are
This file used to define subsumes_chk/2
, but this is now a built-in
predicate:
subsumes_chk(
+General,
+Specific)
There are currently two predicates in this file:
subsumes(
?General,
+Specific)
variant(
?Term1,
?Term2)
variant(
Term1,
Term2)
holds precisely when
subsumes_chk(
Term1,
Term2)
and
subsumes_chk(
Term2,
Term1)
both hold.