in metaKB, keep track of where discovered theories come from;
in rewriting, allow TRS and FRS to return a list of rules used
to normalize in addition to the normal form of a term/formula