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

点击翻译按钮获取中文摘要

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