用語索引

コンピュータサイエンスでは、用語インデックスは、論理プログラム、^{[ 1 ]}演繹データベース、または自動定理証明器内の用語や節の高速検索を容易にするためのデータ構造です。

自動定理証明器における多くの操作は、膨大な数の用語と節の集合内での検索を必要とする。このような操作は通常、次のスキームに分類される。集合が与えられた場合${\displaystyle S}$用語（節）とクエリ用語（節）${\displaystyle q}$見つける${\displaystyle S}$一部/すべての用語${\displaystyle t}$関連する${\displaystyle q}$ある特定の検索条件に従って。最も興味深い検索条件は、クエリと取得オブジェクトを特別な方法で関連付ける置換の存在として定式化される。${\displaystyle t}$以下は、証明器でよく使用される検索条件の一覧です。

• 学期${\displaystyle q}$用語と統一可能${\displaystyle t}$つまり、置換が存在する${\displaystyle \theta }$、したがって${\displaystyle q\theta }$=${\displaystyle t\theta }$
• 学期${\displaystyle t}$は${\displaystyle q}$つまり、置換が存在する${\displaystyle \theta }$、したがって${\displaystyle q\theta }$=${\displaystyle t}$
• 学期${\displaystyle t}$は一般化である${\displaystyle q}$つまり、置換が存在する${\displaystyle \theta }$、したがって${\displaystyle q}$=${\displaystyle t\theta }$
• 句${\displaystyle q}$θ-包含節${\displaystyle t}$つまり、置換が存在する${\displaystyle \theta }$、したがって${\displaystyle q\theta }$は、${\displaystyle t}$
• 句${\displaystyle q}$θは​${\displaystyle t}$つまり、置換が存在する${\displaystyle \theta }$、したがって${\displaystyle t\theta }$は、${\displaystyle q}$

多くの場合、私たちは取得した用語とともに、適切な置換を明示的に見つけることに興味があります。${\displaystyle t}$単にそのような置換の存在を確立するだけでなく。

検索対象となる用語セットのサイズは大きく、検索呼び出しは頻繁で、検索条件テストはかなり複雑であることが多い。このような状況では、線形検索は${\displaystyle S}$検索条件が各用語に対してテストされる場合${\displaystyle S}$そうなると、非常にコストがかさむことになります。この問題を克服するために、高速検索をサポートするインデックスと呼ばれる特別なデータ構造が設計されています。このようなデータ構造と、インデックスの維持および検索のための付随アルゴリズムを合わせて、用語インデックス作成技術と呼びます。

• 判別木
• 置換木
• パスインデックス作成

置換木は、パスインデックス、判別木インデックス、および抽象化木よりも優れた性能を発揮します。^{[ 2 ]}

判別ツリーの用語インデックスは、その情報をトライ木データ構造に格納します。^{[ 3 ]}

第一引数インデックス付けは最も一般的な手法であり、第一引数をインデックスとして使用します。これは、原子値と複合項の主関数を区別します。

非第一引数インデックス付けは、第一引数インデックス付けの変形であり、第一引数インデックス付けと同じ、または類似の手法を1つ以上の代替引数に適用します。たとえば、述語呼び出しで第一引数に変数を使用する場合、システムは代わりに第二引数をインデックスとして使用することを選択する場合があります。

複数引数インデックスは、十分な選択性を持つ単一引数インデックスが存在しない場合、インスタンス化された複数の引数に対して結合インデックスを作成します。

ディープインデックスは、複数の節が何らかの引数に対して同じ主関数を使用する場合に用いられます。これは、複合項の引数に対して、同じまたは類似のインデックス手法を再帰的に適用します。

トライインデックスは、プレフィックスツリーを使用して適用可能な節を検索します。^{[ 4 ]}

• P. Graf、「用語索引付け」、Lecture Notes in Computer Science 1053、1996年（やや古い概説）
• R. Sekar、IV Ramakrishnan、A. Voronkov、「用語索引付け」、A. Robinson、A. Voronkov編、『自動推論ハンドブック』第2巻、2001年（最新概説）
• WW McCune、「用語検索のための判別木インデックスとパスインデックスの実験」、Journal of Automated Reasoning、9(2)、1992年
• P. Graf、「置換ツリーインデックス」、RTA論文集、Lecture Notes in Computer Science 914、1995年
• M. スティッケル、「用語索引付けのためのパス索引付け法」、技術報告書473、人工知能センター、SRIインターナショナル、1989年
• S. Schulz、「特徴ベクトルインデックスを用いたシンプルかつ効率的な節包含」、IJCAR-2004ワークショップESFOR論文集、2004年
• A. Riazanov、A. Voronkov、「部分適応型コードツリー」、JELIA論文集、人工知能講義ノート1919、2000年
• H. Ganzinger、R. Nieuwenhuis、P. Nivela、「コード化されたコンテキストツリーを用いた高速用語インデックス作成」、Journal of Automated Reasoning、32(2)、2004年
• A. Riazanov、A. Voronkov、「標準パスインデックスとリレーショナルパスインデックスを用いた効率的なインスタンス検索」、Information and Computation、199(1–2)、2005年