高速推論を目的とする一階論理コンパイラに関する研究

本研究では、一階論理の高速推論を目的として、一階論理式を機械語プログラム翻訳し計算機上で直接実行させるための、一階論理コンパイラの研究・開発を行った。本コンパイラは証明すべき一階式が与えられたとき、まずその上の順序付線形導出法を模倣するPrologプログラムを生成する。次に証明中で生成される冗長な節や恒真節の消去を目的とした枝刈コードの挿入など幾つかの最適化処理を行い、最終的にPrologコンパイラを用いて機械語プログラムへ変換する。実験により、初期の目的であった1桁以上の高速化が達成されたことを確認している。また本研究では補題(1emma)処理に関しても研究を行った。既在の研究により、補題の導入は重複計算の抑制に非常に有効であることが示されているが、逆に探索空間の増大をもたらす欠点の知られている。本研究では、不必要な探索空間の増大を抑制する目的として、現代的なPrologシステムに備わっている遅延演算子を利用した実行メカニズムを開発した。これは変数代入を極力抑制し、複数の探索パスを統合化(一本化)することにより、探索空間の縮小を図るものである。実験により、かなりの効果があることを確認している。

本研究では、一階論理の高速推論を目的として、一階論理式を機械語プログラム翻訳し計算機上で直接実行させるための、一階論理コンパイラの研究・開発を行った。本コンパイラは証明すべき一階式が与えられたとき、まずその上の順序付線形導出法を模倣するPrologプログラムを生成する。次に証明中で生成される冗長な節や恒真節の消去を目的とした枝刈コードの挿入など幾つかの最適化処理を行い、最終的にPrologコンパイラを用いて機械語プログラムへ変換する。実験により、初期の目的であった1桁以上の高速化が達成されたことを確認している。また本研究では補題(1emma)処理に関しても研究を行った。既在の研究により、補題の導入は重複計算の抑制に非常に有効であることが示されているが、逆に探索空間の増大をもたらす欠点の知られている。本研究では、不必要な探索空間の増大を抑制する目的として、現代的なPrologシステムに備わっている遅延演算子を利用した実行メカニズムを開発した。これは変数代入を極力抑制し、複数の探索パスを統合化(一本化)することにより、探索空間の縮小を図るものである。実験により、かなりの効果があることを確認している。