研究の内容

前年度の成果をベースに以下の項目について研究及び開発を進めた。

1. ケース分割の冗長性除去手法：ケース分割によって生じる二つの冗長性 を削除する手法をMGTPに組み込んだ。削除される第一の冗長性は、分岐後の 各枝で重複して同じ証明を行ってしまう重複証明、第二の冗長性は、分岐そ れ自体が証明には関連(寄与)していない無関連分岐である。また、この第二 の冗長性に対処するNHM(前年度の研究成果)を評価し、新たに幾つかの方式 を考案し実装した。
2. 高速検索機能：MGTPの基本演算である連言照合と包摂検査を高速化する ための弁別木プログラムを作成した。
3. 項書換え処理の導入：項書換え処理をMGTPに組み込むことにより、項書 換え規則による問題記述が可能となった。
4. GAの定理証明への組み込み：事例研究として、Condensed Detachment問 題をGA風戦略を取り入れたMGTPで解く手法の検討を行なった。
5. GUIシステム：MGTPの実行や統計情報の表示をサポートするウィンドウ マネージャを作成した。
6. その他：インタプリタ版CMGTP、MG問題ファイル解析プログラムを作成 した。また、前年度の成果ソフトウェアのバグ改修、機能拡張を行った。