术语索引

在计算机科学中，术语索引是一种数据结构，用于促进逻辑程序、演绎数据库或自动定理检验器中的术语和条款的快速查找。

自动定理证明器中的许多操作需要在巨大的术语和条款集合中进行搜索。这类操作通常分为以下几种情况。给定一个集合根据某种检索条件。大多数有趣的检索条件被表述为存在一个替换，该替换以一种特殊的方式将查询和被检索的对象联系起来的子集/子多集。更多的时候，而不是仅仅为了确定这种替换的存在。很多时候，需要搜索的术语集规模很大，检索调用频繁，检索条件测试也相当复杂。

中的线性搜索，当检索条件被测试在每一个术语上时，每一个术语进行测试时，在S中进行线性搜索的成本过高。为了克服这个问题，我们设计了特殊的数据结构，称为索引，以支持快速检索。这样的数据结构，以及伴随的索引维护和检索算法，被称为术语索引技术。

鉴别树替换树路径索引替换树的性能优于路径索引、鉴别树索引和抽象树。鉴别树术语索引将其信息存储在一个trie数据结构中。