Logtk.DtreeSourceThis module provides a simplification index, based on a perfect discrimination tree (see "the handbook of automated reasoning", chapter "term indexing", for instance).
The simplification index can only retrieve generalizations of a given query term, but it does it efficiently.
It is used for demodulation (rewriting) in Superposition.