平成8年度 委託研究ソフトウェアの提案

(11) KLIC 上の MGTP 処理系

研究代表者:長谷川隆三 教授
      九州大学大学院 システム情報科学研究科知能システム学専攻




[目次]

  1. 研究体制
  2. 2年目の研究内容
  3. 想定されるソフトウェア成果

[研究体制]

      氏名         所属
研究代表者 長谷川隆三 九州大学大学院システム情報科学研究科教授
研究協力者 藤田 博  九州大学大学院システム情報科学研究科助教授
研究協力者 越村 三幸 九州大学大学院システム情報科学研究科助手
研究協力者 久保山哲二 九州大学大学院システム情報科学研究科博士後期課程3年
研究協力者 田中 智浩 九州大学大学院システム情報科学研究科修士課程2年
研究協力者 松本 誉史 九州大学大学院システム情報科学研究科修士課程2年
研究協力者 井上 克巳 豊橋技術科学大学情報工学系助教授,p>

[2年目の研究内容]

前年度に得られた研究成果をベースに,以下の項目について研究および開発を 進める.

(a) 既システムの整備:利用効率を高めるために各種オプションを整えると共 に,インストール手順の簡便化を計る.また,コンパイル版MGTPのコンパイル 時間削減手法を考察する.

(b) NHMの評価・改良:前年度に実装した深さ優先NHMについて,その枝刈り効 果を定量的に調べると共にNHM変換の効率化手法(変換節数の削減や制御用アト ムの取り扱いなど)の開発を進める.また,幅優先NHMについても実装を行う.

(c) MGTPプログラミング環境の開発:前年度に作成したMGTP実行のトレーサを 基にMGTPの実行過程を視覚的に表示する機能を実現する.各種統計情報の他に, MGTP証明図や連言照合計算を視覚化対象とする.証明図については,証明図変 換により(無駄な推論を省いた)簡単化したものも視覚化できるようにする.視 覚化プログラムは,可搬性を考慮してTcl/TkもしくはPerl/Tkを用いて試作を 行う.

(d) MGTPによる記述実験:MGTP(または制約MGTP)を用いて様々な問題の記述を 試みる.この経験をMGTPの機能拡張および利用技術向上に役立てるように整理 し,MGTPを各種推論システムのプラットホームとして利用できるように強化す る.またMGTPの記述を整理し,MGTP例題集としてまとめる.

(e) 推論速度の高速化:MGTP節からKL1節への変換の最適化,および動的に生 成されるデータへのアクセスを高速化するために基本ルーチンの速度向上を計 る.またケース分割の重複削減手法として知られるフォールディングアップ法 をMGTPに取り入れその効果に関して実験を行う.

(f) 等号の導入:等号推論をMGTPに導入し,MGTPの記述性能を高める.現在の MGTPでは等号を扱う場合,等号に関する性質を規則として入力する必要があり, 等号の導入により記述量の削減と処理速度の向上を図ることができる.

(g) その他:インタプリタ版MGTP(前年度に作成)の手法をCMGTPにも適用し, インタプリタ版CMGTPの開発を行う.KL1コードがMGTP節に埋め込まれている場 合の処理法についても検討する.また,KLIC上でプログラミングを進めていく 上で有用なツールやライブラリ群を適宜作成していく.これらはMGTP開発の効 率を高めることのみならず,一般のKLICプログラマにも便宜を図ることを目的 とする.

【TG活動計画】

IFSに登録されているMGTP関係のソフトウェアの利用者および開発者間で、利 用形態、実行環境、強化・付加すべき機能等に関する意見を交換し、共通の課 題について検討・分担しIFSへフィードバックすることを目的とする。

具体的には、ノンホーンマジックセット法の変換手法やモード解析の効率化手 法、様相推論、制約MGTPの機能向上などの研究項目および、プログラミングシ ステムとしてより使い易いMGTPシステムを目指し意見を交換する。後者につい ては、demodulatorの組込みやMGTP節→KL1節変換の最適化などの開発項目を想 定している。

今年度は、年2回程度の開催を予定している。


[想定されるソフトウェア成果]

(1)作成されるソフトウェア名称

KLIC-MGTP & KLIC-RUN 

(2)そのソフトウェアの機能/役割/特徴

MGTPの基本機能は(一階の)入力節集合のモデルを枚挙することである.枚挙に はもれがないので(完全性),枚挙されたモデル数が0の時は,与えられた節集 合は充足不可能であることがわかる.このことからMGTPは,一階の定理証明系 として使用できることが分かる.

モデルは,節集合を満たす領域(集合)であるから,問題の解が満たすべき条件 (制約)を節集合で記述した場合,枚挙されたモデルは,解そのものとなる.モ デルは節の入力順に依存せず求まるので,宣言的に問題の解法が記述できる.

一方,MGTPの入力節は,条件式とその成立時のアクションを記述したものと手 続き的に解釈することができ,MGTPをプログラミング言語とみなすことができ る.このことは,MGTPの潜在的な能力の高さを示しており,実際に推論系記述 言語として利用されている.またユーザは,並列実行の為の指示をMGTPの節記 述に埋め込むことができる.

このようにMGTPでは,宣言的記述と手続き的記述の双方が可能である.また, KL1では失われた完全性を保持しているのにもかかわらず,計算機構は極めて 単純な原理に基づいており,プログラムがコンパクトで手を加え易いのが特徴 である.この単純さが故にMGTPには,様々な使いよう(汎用性)があるのである. MGTPはそれ単体のみではなく,より大きなシステムの部品として利用する事も できるオープンなシステムである.

さらに,否定制約や等号に関する推論を組み込んでおり,自然な問題記述が可 能である.また,実行トレーサや証明図視覚化ツールなどのプログラミング環 境も用意されている.

KLIC実行環境(KLIC-RUN)においては,できるだけLispやPrologのような感覚で ユーザ定義述語の走行・デバッグを行える機能を備える.また,入出力に関す るユーティリティの整備を図る.

(3)ソフトウェアの構成/構造

システムは大きく三つの部分,(a)変換部,(b)推論部,(c)表示部に分けられ る.変換部で変換されたユーザ入力節は,推論部とリンクして走行し,表示部 が走行結果を示す.

(a) 変換部
記述言語は,KLIC.ユーザ入力節をKL1節に変換する.変換に先だって,スタ イルチェックを行うこともできる.ある種のバグはこの段階で見つけることが できる.NHM変換の指示はこの段階で行う.

(b) 推論部
KL1節に変換された入力節は,KLICコンパイラによってKL1で書かれている推論 部とリンクされる.幾つかの連言照合方式があり,ユーザはオプションにより推論 方式を指定する.否定制約や等号に関する推論も組み込まれている.また,ユー ザ入力節を直接解釈し推論を行うインタプリタ版もあり,変換時間を節約できる.

並列化方式も備え付けのものをオプションで指定できる.また,トレーサは走 行時のオプションによって起動される.

(c) 表示部
走行時のオプションによって,可視化に必要なログ情報が収集される.ログ情 報に基づいて,実行及びモデルの可視化が行われる.表示部は,X上で構築さ れる.

(d) KLIC-RUN
基本的には,必要な機能をシェルコマンドとして実現し,これらをシェルスク リプトで制御する.必要に応じてKLICコンパイラに手を加える事も検討する.

(4)参考とされたICOTフリーソフトウェアとの関連

KLIC-MGTPは,既に登録してあるIFSの機能拡張版である.KLIC-RUNについては, IFSに新規登録する.

(5)使用予定言語および動作環境/必要とされるソフトウェア・パッケージ/ポータビリティなど

(a) マシン:Sparc Station,並列UNIXマシン,PIM/m,DOS/Vマシン
(b) OS:Solaris2.X,PIMOS,Linux 
(c) 使用言語等: gcc,klic,perl,tcl/tk 

(6)ソフトウェアの予想サイズ(新規作成分の行数)

20K

(7)ソフトウェアの利用形態

定理証明システムとして開発されてきたMGTPは,数学的定理を証明するシステ ムに留まらず,一種のプログラミングシステムとして利用される事を念頭にお いて開発される.

必要とされる推論規則をMGTPの規則として書き下すことにより,知識表現言語 の推論エンジンや各種人工知能応用の推論システムとして利用することが可能 である.MGTPは一種のメタプログラミングシステムとみなす事ができ,上記に 述べたように汎用性に富む.

KL1で書かれているので並列UNIXシステムの上で容易に並列性を抽出する事が できる.また,MGTP上で個々のエージェントを実現することにより,分散AIシ ステムの実験などを行う事もできよう.

MGTPの推論核部分は,コンパクトなので,ユーザの目的に合わせて必要部分を 高速化したり,また並列探索の為の制御部分を変更する事が容易である.

(8)添付予定資料

開発したソフトウェアについては,ソフトウェア仕様書,ユーザマニュアルを 添付する予定である.


www-admin@icot.or.jp