(14) KLIC 上の MGTP 処理系に関する研究

［中間報告］

(１) 研究進捗状況

可搬性を高めるために，Prolog上で稼働していたMGTP変換プログラムをKLICに 移植するとともに変換プログラム内でのモジュールの共有化を図っている．

また，探索空間の枝刈りによって証明時間を短縮するNHM(ノンホーンマジック セット)法をMGTPの前処理システムとして提供することにし，前処理システム としてNHM機能の他に提供できる機能の検討も行った．

使いやすさの向上のために，MGTP実行のトレーサやデバッガの機能を検討する とともに，ビジュアルな表示も可能とするためにTcl/Tk上のGUIベースのプロ グラムとの結合を考慮しTcl/Tkの調査を行った．

(２) 現在までの主な成果

KLIC上のプログラムとして動いているものは以下の通り．

1) MGTP/G(RAMS版)の変換プログラム(今までは，Prolog上で動いていた)
2) 定理証明問題集TPTP(数千題を所蔵)の問題をMGTP節に変換するプログラム
3) MGTP節が値域限定を満たしているかどうかをチェックするプログラム(MGTPは値域限定を満たしている問題の証明を得意としている)
4) KLICでの開発効率を高めるKLIC_RUNシステムの一部プロトタイプ：コンパイラベースのKLICで，インタープリタベースのLispやPrologのような開発環境を提供する．

(３) 今後の研究概要

先ず，MGTPの推論部内でのモジュールの共有化を図り，コードサイズを縮める． それと共にトレーサ用の手続きをコードに埋め込み，これを試用する．試用経 験を踏まえ，また外部の利用者の意見なども参考にし，トレーサの改良を試み る．トレース情報を文字情報のみならず図形情報としても表示できるように， Ｘウィンドウシステム上に表示システムを作成する．

NHM変換プログラムを作成する．このプログラムには，変換前に比べ変換後に は指数オーダで増加するデータ(MGTP節集合)のサイズを削減するためのMGTP節 集合のモード解析プログラムが組み込まれる．NHM変換による証明時間短縮効 果を測定すると共に，モード解析によるデータ削減効果についても調べる．測 定結果を元に定性的な考察を行う．また，値域限定を満たさない問題を値域限 定を満たすよう変形するプログラムを作成する．

(４) 今年度目標成果（イメージ）

成果物として完成予定のソフトウェアのイメージは次の通り．

1) MGTPシステム(プロトタイプ)一式：前処理部，変換部，推論部，図的情報 表示部からなり全てKLIC(もしくはC)上で稼働する．前処理部は，TPTP問題変 換器，値域限定性チェッカ，値域限定変型プログラム，NHM変換器からなる． 推論部にはトレース機能が組み込まれ，起動時のオプション指定により利用で きる．トレース情報はグラフィカルにも表示することができる．

2) KLIC_RUNシステム：ガード述語とボディ述語(ユーザ定義述語を含む)の実 行を対話的に行うことができる簡易実行環境である．その他共通に使用される ライブラリ群を含む．