(3)Java-MGTPと高度推論機構の開発

研究テーマ、研究代表者：

(1)研究テーマ

(2)研究代表者(氏名、所属、役職)

報告項目

(1) 研究の目的

前年度の成果であるＪａｖａ−ＭＧＴＰについて，i)機能及び性能面に関する 改良，ii)並列化による速度向上，iii)ＭＧＴＰ向きの探索制御法の確立，を 図かり，高速で操作性に優れた魅力的なシステムを提供することを目的とする．

(2) 研究の進捗状況

これまで，正制約のみを扱うＭＧＴＰと正/負制約を扱うＣＭＧＴＰの二本立 てでシステムを提供してきたが，ＣＭＧＴＰに一本化を図った．従来のＣＭＧ ＴＰで正制約のみの問題を解かせた場合，ＭＧＴＰに比べて格段に証明性能が 劣っていたが，これを解消した．主な改良項目は，ア)多重環境下での環境切 替えの高速化，イ)データの登録と検索を高速化するための弁別木機構の組込 み，ウ)節(通常の言語処理系では関数に相当)インデキシング機構の導入，で ある．またウ)に関連して，節の構文を拡張し問題の記述能力を高めた．これ らの改良を施した結果，従来のＪａｖａ−ＭＧＴＰに比べ，数倍から十倍の性 能向上が達成できた．

以上の他に，a)リアルタイムに証明木を表示(これまでは証明終了の後に表示 していた)するための推論部と表示部のマルチスレッド化，b)EmacsLispによる MGTP編集モードの作成，c)分離の規則を含む問題による探索制御法の評価，d) 区間制約処理のための予備実験，e)畳込み(補題生成による探索空間の刈込み) 機能のＣＭＧＴＰへの導入，f)畳込み機能を備えたＭＧＴＰのＮ逐次実行方式 による並列化，を行っている．

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

• Ｊａｖａ−ＣＭＧＴＰの高速化とその評価
• Ｊａｖａ−ＣＭＧＴＰの問題節の構文拡張

(4) 今年度目標成果ソフトウェアイメージ

ＷＷＷブラウザがＭＧＴＰの基本ユーザインターフェースとなる．システムの 試用とダウンロードができるホームページを開設する．証明が進むにつれて証 明木が図示され，証明終了後には数々の統計情報が表示される．証明木は必要 に応じて拡大・縮小することができる．また証明途中で証明を中断し，それま での証明過程をナビゲーションすることもできる．証明再開にあたっては，探 索法の変更や探索の省略などを指示できる．このような図的インターフェース の他に，従来のコマンドラインによるインターフェースも提供し，バッチ的処 理も行える．