(15) MGTP における推論制御と探索問題への適用

ボトムアップ型の定理証明器MGTPは，フルの一階述語論理を扱うことができる が，non-Horn 節プログラミングのための技法はまだ十分開発されているとは 言えない．そこで本研究ではまず，反復深化深さ優先(DFID)探索をMGTPの探索 戦略とすることで，停止性の向上を図った．次に，選言肢にコストを付加した コスト付ノンホーン節を採用した汎用の論理プログラミング言語を提案し， その処理系をMGTPを利用して開発した．また，コスト付の問題をうまく解くこ とができるように，MGTPの探索戦略として，反復深化最良優先(BFID)探索を 組み込み，最適化問題に応用した．さらに，最適化問題の効率化のために， 定理証明分野で用いられているノンホーン・マジックセット法を応用し， ゴールに関連するボトムアップ推論のみに探索を絞ることを可能とした．

研究の期間：

１９９７年６月１日 より １９９８年２月末日

研究協力者：

羽根田博正	神戸大学工学部　教授
関山 順一	豊橋技術科学大学大学院工学研究科　修士２年
鍋島 英知	豊橋技術科学大学大学院工学研究科　修士２年
長谷川隆三	九州大学大学院システム情報科学研究科　教授