特に、法律分野の推論のような不確実な知識を含む領域においては、 仮説の組合わせが膨大な探索空間の爆発を引き起こすため、 探索を効率化させるための推論制御技法ならびに実装技術としての 効率化技法は、極めて重要な要素である。
正負リテラル、ならびに様相オペレータに関する一貫性制約は、あらかじめ入 力節として与える方法があるが，入力節が膨大になり、連言照合による計算量 が増大する、また、様相オペレータを相異なる述語記号として扱うと、項メモ リのメモリ使用量が増大し、かつ登録/参照のコストも増加するなどの問題が ある。
MGTP では、こうした問題を解決するために、同じ述語に対する正負記号 ならびに様相記号を述語に対する属性と考え、単位反駁によるモデル候補の早 期棄却と、選言の簡約化によるモデル拡張爆発の抑制を可能とした。
同じ述語上の属性の両立関係は， 下の表にまとめられる． 表中、×は、縦軸の属性と横軸の属性が両立しないことを表し、 ◯は両立可能であることを表す。
なお、上記の両立関係の検査は、後述する 活性化情報によって効率的に実装されている。
【実装方式の概略】
Java MGTP では、 最も基本的なデータ構造となる項は抽象クラス Term を継承する クラスのインスタンスオブジェクトであり、後述する活性化セルや 項メモリ上での探索ポインタを属性として保持する。 特に活性化セルの導入により、同じ項はいかなる文脈においてもすべて同じ オブジェクトにより表される点が大きな特徴である。 これにより、定理証明システムにおいて効率上のボトルネックとなる 包摂検査や照合手続きを高速化することができた。
【分岐時の環境複製】
非ホーン節、A1, ..., An -> C1; ...; Cm が適用されることにより、現モデル候補 Mは M∩{C1}, .., M∩{Cm} の m 個のモデル候補に拡 張され、各々のモデル候補ごとに推論が進められる。 各モデル候補の推論は独立、平行に進めてよいので、 環境を複製する必要性が生じるが、 M が大規模になると、 構造の複製は高価である。そこで、 共用できるデータに対しては複製を極力避けるために、 モデル候補 M の表現として下図に示したような Last-In-First-Out構造を採用した。
【活性化情報】
一般に集合 S に対する要素 e の所属検査 e ∈ Sを高速に行うには、 例えばハッシュ法を利用すればよい。場合分けの結果、複数のモデル候補 Mi に対する同一リテラル L の所属検査 L ∈ Miを行う必要があるの で、ハッシュ法だけでは不十分である。
モデル生成法に基づいて構成されるモデル候補は、 非ホーン節による場合分けに対応する分岐点を有し、 ホーン節拡張によるアトム集合でラベルづけされる枝から成る 木構造を形成する。 この木の根から一つの葉に至る枝上の点列が、一つのモデル候補に対応する。
こうして、複数のモデル候補が同一リテラルを共有する状況がある。 逐次実行のもとでは下図 (b)に示すように 二重線で表された枝に対応する一つのモデル候補のみが対象 (active) となり、 白丸で表されたリテラルの所属検査が問題とされる。
active なモデル候補に含まれる枝の A-セルの値は true であり、 その状態を A_S◯ と表す。 過去 active であったモデル候補に含まれる枝の A-セルの値は false であり、その状態を A_S● と表す。 各モデル候補 M には、それが含む枝のすべての A-セルからなるリスト AL_M を割り当てる。 モデル候補 M が証明木の根から順に枝 S1,...,Snを含むとき、 M の A-セルリスト AL_M を
モデル候補 M が active のとき、 AL_M を active な A-セルリストという。
アトム A には、正負および様相オペレータに関する情報を 属性として割り当てる。アトムの所属検査や両立不能な属性の 有無を検査する際には、これらのアトムの属性を検査するだけで良い。 また、異なる分岐へ制御ポイントが移動する際も、A-セルの状態変更を 行うだけで複数のリテラルを一斉に inactive に変更することができる。
【照合】
照合(match) は、生成されたモデル候補(およびモデル拡張節)と前件部の 単一化を行い、単一化可能な場合には、後件部を新たなモデル拡張候補として 出力する操作である。
照合機能は、モデル生成型推論において、最も実行時間に影響を与える 機能であり、効率的な実装技法が要求されるが、 A-セルの導入により、すでにモデル候補に加えられている項と 前件部の基底項との照合は、単にA-セルを参照するだけで 済む。
また、前件部が変数項である場合には、束縛値の扱いが問題となる。すなわち、 二つの項の照合の結果、変数がある値に束縛される場合、変数とその束縛値の 対応を如何に内部表現するか、また、同じ変数名の別の出現に対し、束縛情報 を如何に伝達するか、という問題である。
Lispの A-list のような <変数, 束縛値> の対を別の領域に もつ方式は、項は常に変数束縛情報(環境)を参照して扱われなければならず、 記述が繁雑で実行も遅くなる。そのため、本システムでは、記述を簡単にし、 実行を速くするために、変数オブジェクトが直接その束縛値を属性として 参照できる方式を採用している。
また、変数項に対して照合可能な基底項の探索は、次に示す Skip-list を用いて効率的に実現した。
【項メモリとSkip-list】
項の登録を行う項メモリは、項を平坦な記号列と捉えて、階層構造を経路として 表現したものであり、 下図に示すように、共通部分を共有した 木構造(弁別木)となっており、データの格納、マッチング、データ検索を効率良く 行うことができる。
連言照合の際には、 非基底の前件リテラル p(X) と照合可能な基底リテラルの探索は、 弁別木を（active ノードを選択的に）走査して行うことになる。 上図で、前件リテラル p(X,Y) のもとに照合が開始されたとする。 p の照合成立の後、 変数 X に対する基底代入には f(a,b) と f(d,b) の可能性がある。 これは、関数記号 f に付随する Skip-list によって知ることができる。 まず、σ={X/f(a,b)} としたときの照合の続行点は b_1◯ ノードであり、引続き {Y/c} で照合が成立することが分かる。 次に、σ={X/f(d,b)} とすれば、 b_2◯ ノードを続行点として {Y/e} で照合が成立することが分かる。