内部変数消去ためのエルブラン領域での全展開法

概要

論文の詳細を見る
一階述語論理の半非決定性のため、任意の基礎原子式A∈B_p:エルブランベースを入力とし有限時間内にAがプログラムPの論理的帰結であるか否かを答えるアルゴリズムは存在しない。そこで、Clarkにより、失敗を否定と見なす規則(Negation As Failure)が提案されている。その規則は実現しやすいという理由でPrologなどの論理プログラミング言語で使われている。しかし、この規則で、述語の変数を束縛できるのは正の述語の呼出しが成功したときだけである。どのように負述語に現れる変数の束縛を計算するかが興味深い問題である。有力な手法の一つは佐藤氏の提案した否定技法である。しかし、否定技法は内部変数を含むプログラムに適用できない。そこで、我々は与えられた確定節プログラムをそれと等価な内部変数なしのプログラムへ変換する手法を考えてみる。本論文では、最小モデル不変の意味で、一般的な内部変数を含む再帰節に対するエルブラン領域での全展開法を提案する。
一般社団法人情報処理学会の論文
1989-03-15