CMGTPは、MGTPに負情報に関する処理を加えたものである。従来のKLIC-CMGTP では複数の箇所で簡約化・反駁手続きが行なわれていた。各箇所の簡約化手続 きの有無と枝刈り効果の関係を調べた結果、モデル拡張候補集合から要素(Δ) を取り出す場合のみ簡約化を行なうと最も効率的であると判明した。また、Δ の取り出しは単位節優先で行われるが、従来は単位節を取り出す度に簡約化を 行っていた。しかし、単位節がつき、選言が取り出されるときのみ簡約 化を行うのが有効と考えられる。
これらの方針に従いKLIC-CMGTPの改良を行なった。
次に、
このKLIC版の改良を反映しつつJavaへの移植を試みた。 定理証明系の例題を用いた比較実験から、従来のKLIC-CMGTPに比べ、改良版 KLIC-CMGTPでは、2/3から半分近くまで証明時間が短縮された。また、 Java-CMGTPと改良版KLIC-CMGTPとを比較では、ほとんどの場合にJava-CMGTPの 方の実行速度が速いことが分かった。ただ、Java-CMGTPにはモデル拡張候補集 合中の選言バッファに対してcloneを作るという操作のオーバヘッドがり、証 明時間が短いときにはこれが無視できずKLIC-CMGTPの方が速くなることもあっ た。