Next: 5.4 論理変数の調査
Up: 5 Prolog処理系の実現
Previous: 5.2 データベースへの登録
ホーン節のデータベースにおいてあるゴールが与えられ，そのゴールを証明す
る手続きをproveとする．proveの処理手順は次のようになる．
まず，与えられた問い合わせゴールの述語をもつホーン節の集合を取り出す．
それらすべてについて，順に問い合わせゴールと節のヘッドとのマッチン
グがなされるかどうかを調べる．ひとつの節のヘッドとマッチングした場合
には，ここでのマッチングは，互いのパターンに変数が入っているためにunify
を使わなければならない．
unifyの結果は変数のバインディング情報であり，そのバインディング情報を
もとに，条件部（節のボディー部）の述語をすべてゴールとして証明を続ける．
proveとprove-allは互いに参照する再帰型の手続きになっている．与えられ
たゴールがすべてなくなった場合には証明が終了したことになり，バインディ
ング情報を返す．途中でunifyが失敗した場合には，nilを返す．
(defun prove (goal bindings)
(mapcan
#'(lambda (clause)
(let ((new-clause (rename-variables clause)))
(prove-all
(clause-body new-clause)
(unify goal (clause-head new-clause)
bindings))))
(get-clauses (predicate goal))))
(defun prove-all (goals &optional bindings)
(cond
((eq bindings 'fail) nil)
((null goals) (list bindings))
(t (mapcan
#'(lambda (goal1-solution)
(prove-all (rest goals) goal1-solution))
(prove (first goals) bindings)))))
ここでの重要なポイントとして，証明しようとしているゴールと次々にたどら
れるホーン節の中の変数名が同じであるとまちがいが起こることがあげられる．
入力された変数名は同じであっても内部では異なる変数として扱われなければ推
論が継続できなくなる．そこで，上にあるように，ホーン節の中にでてくる変数す
べての名前を他の節の名前とぶつからない名前に変更する必要がある．
generated through LaTeX2HTML. M.Inaba 平成18年5月7日