コンパイルに基づくサーカムスクリプションの高速な定理証明手法

1994 Fiscal Year Annual Research Report

• Project/Area Number: 06780304
• Research Institution: University of Yamanashi
• Principal Investigator: 岩沼 宏治 山梨大学, 工学部, 助教授 (30176557)
• Keywords: サーカムスクリプション / 極小限定 / 推論 / 定理証明 / コンパイル

Research Abstract

本研究では、不完全情報の常識推論手法を実用化を目的として、サーカムスクリプションの高速推論手法について研究を行なった。より具体的にはサーカムスクリプションのPrologプログラムへの変換、更に機械語プログラムへ変換するコンパイラについて研究を行なった。コンパイルによって、サーカムスクリプションを機械語プログラムとして実現でき、証明計算の高速化が達成された。個別研究項目は以下の通りである。
1.Prologコードへのコンパイル原理とコンパイル・アルゴリズムの確立:生成したPrologコードの推論の相対的完全化が難しい課題であったが、キューを明示的に利用してfairな計算を実現し、解決した。キュー操作のための制御コードを考察・開発し、コンパイル・アルゴリズムを開発した。
2.最適化手法の確立:Prolog言語ソースレベルでの最適化法として、インライン展開法を考察した。性能評価実験により、かなりの効果が確認された。
3.コンパイラの実装とそれを用いた高速化の実証:与えられたサーカムスクリプションをPrologプログラムへ変換するコンパイラの実装を行なった。性能評価実験の結果、既存の手法より10倍程度高速であることが確認された。

Research Products

• [Publications] K.Iwanuma: "Conservative Query Normalization on Parallel Circumscription" Lecture Notes in Artificial Intelligence. 814. 296-310 (1994)
• [Publications] K.Oota: "一階理論に対する単一名公理の計算法" 日本ソフトウェア科学会論文誌:コンピュータソフトウェア. (採録決定).