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ユーティリティ
◎KLIC_RUN
ガード述語およびボディ述語の実行を対話的に行うツール(KLIC_RUNと呼ぶ)を作成した。
◎コマンド読込みツール
ユーザからのコマンドを読み込み解析するプログラムを作成した。本ツールは、
KLICのトークン・リーダとパーサを利用している。KLICでは、項の終りは'.'
(ピリオド)である必要があるが、本ツールを利用すればスペースまたは改行で
よい。