MGTPの基本演算である連言照合と包摂検査を高速に行なうために、KLIC-MGTP では、内部データベースを高速に検索できる弁別木プログラムを利用している。 Java-MGTPの開発に伴って、弁別木プログラムのJava化も行なった。弁別木は、 木の各節点がハッシュ表となっているようなデータ構造をもっている。ハッシュ 表の実装法をいくつか代えて、弁別木の実装を行なった。
ところで、証明が分岐した後の各分枝では、それぞれ独立に弁別木が構築され ていく。データを不変データ型(mutable data type)を用いて実装している KLICでは、データに対する参照透過性があり、ある分枝での弁別木更新の影響 は他の分枝に伝播しなかったので、各分枝で自然に独立に弁別木を構築するこ とができた。一方、参照透過性のないJavaでは、弁別木更新の影響が他の分枝 にも影響してしまう問題があり、なんらかの手段を講じなければならない。そ こで、いくつかの手法を考案し実装した。
それぞれの実装での性能を測定した結果、例題によっては、数倍程度の速度向 上を達成したものの、速度低下を招くものもあり、今後その原因追求と解決策 の考案を行なう予定である。