IFSとして登録されているKLIC版MGTPをベースに以下の項目について研究およ び開発を進めた。
(1)既システムの整備
Prolog上で稼働していたトランスレータをKLICで書換え、可搬性を高めた。さ らにTPTPライブラリの問題形式からMGTP節形式(以下MG節)に変換するプログラ ム、値域限定性を検査するプログラム、値域限定化するためのdom挿入プログ ラムを作成した。
(2)NHMのKLIC上での実装
MGTPの実用性を高めるために重要な、探索空間の枝刈り手法の一つであるノン ホーン・マジックセット(NHM)法をMGTPに導入し、これに基づくNHM変換システ ムをKLIC上に作成した。またその枝刈り効果を定量的に評価した。
(3)ケース分割の重複削減法
ケース分割の際に現れる探索木の重複を極力抑えるため、Letzにより提案され ているフォールディングダウンをMG節の変換によって実現する方式を確立し実 装した。
(4)MGTPプログラミング環境の開発
MG節でのプログラミング効率を高めるために、MGTPトレーサを作成した。この 際にいくつかの実装方式を検討し、その中から汎用性に優れるトレース用KL1 節付加方式を採用した。
(5)インタプリタ方式のMGTPの実装
MG節をKL1節に変換し推論エンジンとコンパイル・リンクする従来のコンパイ ル方式をKLIC上で用いると、Cのコンパイルに多大の時間を要するという問題 があった。この問題を解決するため、MG節を直接読み込みこれを解釈実行する インタプリタ方式の推論エンジンを開発した。また、TPTPライブラリ中の180 題を用いて両方式の性能を比較評価した。
(6)KLICユーティリティ