(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)))))ここでの重要なポイントとして,証明しようとしているゴールと次々にたどら れるホーン節の中の変数名が同じであるとまちがいが起こることがあげられる. 入力された変数名は同じであっても内部では異なる変数として扱われなければ推 論が継続できなくなる.そこで,上にあるように,ホーン節の中にでてくる変数す べての名前を他の節の名前とぶつからない名前に変更する必要がある.