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)))))
重要なここでのポイントとして，証明しようとしているゴールと次々にたどら
れるホーン節の中の変数名が同じであるとまちがいが起こります．入力された
変数名は同じであっても内部では異なる変数として扱われなければ推論が継続
できなくなります．そこで，上にあるように，ホーン節の中にでてくる変数す
べての名前を他の節の名前とぶつからない名前に変更する必要がります．
Next: 5.4 論理変数の調査
Up: 5 Prolog処理系の実現
Previous: 5.2 データベースへの登録
generated through LaTeX2HTML. M.Inaba 平成18年5月21日