| 平成９年度 委託研究ソフトウェアの提案 |
| 研究代表者： | 井上 克已 助教授 |
| 神戸大学工学部 |
MGTP (Model Generation Theorem Prover) は ICOT において開発されたモデル 生成型定理証明システムである。MGTP はフルの一階述語論理における充足可能性 の判定や、節集合の極小モデルの計算を、ボトムアップ型の前向き推論により行う。 フルの一階述語論理を扱えるという点において、MGTP は Prolog では扱えない non-Horn 節をケース分割により取り扱うことができる。
ところが、Horn 節によるプログラミング手法が開発され、各種の応用プログラム が書かれている Prolog と比べると、MGTP における non-Horn 節プログラミングの ための技法はまだ十分開発されているとは言えない。
第１に、MGTP を高速な定理証明器としてではなく、もう一つの重要な側面である、 論理プログラミング分野における選言付論理プログラミング (disjunctive logic programming) のボトムアップ処理系として捉えた場合、各種のプログラミング 技法の整備は必須課題となる。特に、ケース分割により構成される木を用いて、 各種の探索問題が自然に実現できるように、探索方式を整備することが望まれる。
第２に、定理証明器としての MGTP においても、公平な (fair) 戦略を実装して いるとは現状では言えない。例えば、有限のモデルと無限のモデルを持つような 充足可能である節集合では、探索の仕方によっては無限の枝を探索し続けてしまい、 停止しない状況に陥ることがある。これは MGTP が提供している３つの制御戦略が いずれも深さ優先探索を仮定しているためである。
第３に、提案者は過去２年間における再委託研究において、MGTP 上でさまざまな 高次推論体系を実現する処理系を開発してきた。MGTP のケース分割による推論に 着目し、選言付論理プログラミング処理系によるモデル生成エンジンとして MGTP を 使用することで、失敗による否定（非単調推論）・アブダクション・アクション言語 などの高次推論処理系を実現している。このような MGTP 上の応用は、MGTP の 有効性を実証したものと捉えることができるが、適用できる問題のクラスには制限が ある。応用においても、組合せ問題の幾つかは解けるが、コストが付く場合の最適化 問題をうまく解くことはできない。例えば、失敗による否定を用いて、与えられた グラフのハミルトン閉路を求めるためのプログラムを書いて MGTP で計算できる。 しかし、この問題においてグラフの各枝にコストが付いた巡回セールスマン問題に 対しては、決定問題・最適化問題ともにうまい解法を実現することはできない。 同様に、アブダクションにおいて実用上必要となる、コスト付きアブダクションや 確率アブダクションなどの計算も、現在の処理系では全解を求めて比較評価する 以外には計算の方法を持っていない。
このように、MGTP の適用範囲を拡大し、実際の応用問題に使用するためには、 コストや確率に基づいて探索を行う機能が必要となる。
本研究では、MGTP における推論の制御と各種の探索方式の整備を目的とし、 その応用としてコストや確率の情報を持つ組合せ問題や最適化問題などの探索問題 を解くために MGTP に改良を加える。
上記目的のために、MGTP を使った探索プログラミングの手法を幾つか開発する。 具体的には、問題の表現方式として、コストを付加したコスト付 non-Horn 節を MGTP への入力節のシンタックスとする汎用の論理型プログラミング言語を考える。 探索問題や最適化問題はこのプログラミング言語上で宣言的に記述され、コストが 最小または最大となるモデルを発見することで問題が解けるように、MGTP の推論 方式を拡張する。
こうしたコストに基づく最適解探索機能を本研究により開発する拡張 MGTP の上で 実現できれば、提案者が開発してきたMGTP 上のアブダクティブ論理プログラミング 処理系 (ALP-MGTP) や、アクション言語処理系 (Action-MGTP) と併合することで、 将来的にはより高度な問題解決が行えるようになると期待される。
MGTP は既に国際的にもよく知られたモデル生成型の定理証明器であり、かつ 選言付論理プログラミング処理系でもある。本研究の遂行により、その適用範囲は さらに拡大され、MGTP 型探索プログラミング環境が一層整備される。本研究は このように、高度な知識処理システム実現のための知識表現およびプログラミング システムの実現と実用化に大きく寄与するものと考える。
本研究においては、MGTP の推論制御機能の充実と探索問題への応用を図る。 研究内容は、以下の流れに沿ったプログラム開発を行う。
なお、開発する拡張 MGTP は最初は Prolog によりインプリメントする。Prolog を用いる理由は以下の通りである。
（注＊）MGTP における探索制御方式としては、負節や問合せ式の情報に基づく トップダウン制御を組み合わせた NHM 方式をすでに以下の論文で提案している。
これらの研究では、MGTP の応用が演繹データベースや定理証明に絞られており、 一般の探索問題に対する解法を与えているわけではない。本研究においては、 NHM も用いながら、コストに基づく BFID 探索の実現を図る。
| 氏 名 | 所 属 | |
| 研究代表者 | 井上 克已 | 神戸大学工学部 |
| 研究協力者 | 羽根田博正 | 神戸大学工学部 |
| 研究協力者 | 関山 順一 | 豊橋技術科学大学工学部 |
| 研究協力者 | 鍋島 英知 | 豊橋技術科学大学工学部 |
| 研究協力者 | 長谷川隆三 | 九州大学大学院システム情報科学研究科 |
提案者は既に、モデル生成に適した Prolog 版 MGTP を開発しており、 その上での NHM 方式を実装したシステムを作成している。本提案で行う 研究開発は、これらの開発成果であるソフトウェアそのものと、開発で 得た経験やノウハウを活かした形で実施される。また学会未発表ながら、 DFID の MGTP への組み込みもそのプロトタイプ版を作成しており、目的 とする探索機能を持つ拡張 MGTP の実現は十分可能であると考える。
（役割）本ソフトウェアは、より高度な知識処理を実現する知識ベースシス
テムの基礎となる推論制御機構と探索機能を提供している。知識情報
処理システムにとって、探索処理の処理能力はシステムの性能を左右
する大きな要因の一つである。その探索処理の最適化は、実現する
システムに依存する形で行われるべきであり、本ソフトウェアでも
MGTP のケース分割に適したヒューリスティック探索を実現することで、
MGTP が本来持っている高速性を損なうことなく利用している。
このように、ICOT フリーソフトウェアの主要な成果の一つである
MGTP のより効率的な推論方式と、新たな応用方法を提案するという
役割も持っている。
（特徴）MGTP における推論戦略を、従来の深さ優先探索に基づくものから DFID (反復深化深さ優先) 探索に変更したことにより、MGTP の停止 性を向上させている。また、探索問題を宣言的に記述するために、コ ストを持つ一階言語を提供し、これを処理するために MGTP を拡張し ている。さらに、最適化問題を効率良く解くために、Non-Horn Magic Set (NHM) 法を併用して、ゴール（目標述語）に関係するボトムアッ プ推論のみに絞り込み、コストに基づく BFID (反復深化型最良優先) 探索 [仮称] を行う。このようにして、ゴールのコストが最小（最大） となるモデルを効率良く発見することができる。なお、DFID/BFID 探索は問題におけるコストの有無によって切替える。
（ソフトウェア・パッケージ） SICStus Prolog ver.2.1#9 以上
（ポータビリティ） 特別なユーティリティプログラムは不要なので Prolog が動けばほぼ動作すると予想される
（ポイント）定理証明、モデル生成、高次推論、組合せ最適化などの推論や探索を行 わせるために、論理形式で宣言的にプログラムを書いて意図したモデルや最適解を確 認するのに適している。単純なシンタックスであることからＡＩプログラムのプロト タイピングを行うのにも適している。ＡＩや論理プログラミングの研究者のための研 究用、大学・大学院の学生のための知識プログラミングや推論・探索の教育用、さら に一般に知的システム構築用ツールとして広く使うことができる。
www-admin@icot.or.jp