•Prologプログラムは、そのリテラルも節全体もすべてが真理値（true or false）を持つ。述語論理学の論理的意味と自動推論の原理（導出原理と単一化）に基づく手続き的意味は、SLD導出にかんする完全性定理にかかわる。詳しくは成書[10]に譲る。また組み込み述語等はProlog処理系のマニュアルを参考にされたい。
•導出(resolution)は論理学で言う「３段論法」と「背理法」の組合せである。単一化(unification;ユニフィケーション)は、導出を行う際に変数に矛盾のない解を代入すること。背理法ではゴールが正しいことを証明するため、その否定を追加して矛盾を導くことを試みる。 例えば「若者は味噌汁を好まない。」は、ｘは若者であるをp(x)、味噌汁を好むをq(x)とすると、p(y)→q(y) と書けるだろう。このときもp(a)が正しいなら３段論法によりq(a)を得る。
•変数の部分を無視すると、背理法にしたがってｐ→ｑという知識の下でｑを証明しようとすれば、（p→q ）∧ not q ＝ （ not p∨ q）∧ not q ＝ （ not p ∧ not q）∨（ q∧ not q ）＝ （not p∧ not q ） ∨ （矛盾） ＝ not p ∧ not
q となり、pという事実がもし別にあれば矛盾を導く。 きちんと書くと複雑なようだが、Prologで導出をするときはゴールのパタンマッチング（＝ユニフィケーション）手続きの反復である。
•ルール節はq(X):-p(X).となる。もし事実節p(オタマジャクシ).やp(子供(カエル)).がデータベース内にあれば、ゴールq(X)は成功し、 Xがオタマジャクシやカエルの子供とユニファイ（単一化）される。すなわちゴールと同じ頭部を持つ事実やルールを探して、事実なら成功し、ルールなら本体の条件を派生ゴールとして逐次実行する。
•研究史：Prologのしくみを司る導出原理 (Resolution principle) と単一化アルゴリズム(Unificaion algorithm)はJ.R.Robinsonの1965年の論文によってコンピュータによる自動定理証明技術の基礎として確立されたものであり、後にColmerauer、KowalskiによってPrologシステムの推論方式に採用された。1980年代には日本の第5世代コンピュータプロジェクトがPrologシステムをその基幹技術として注目し、自然言語処理、並列コンピュータ、LSI設計等への応用が意図された。
•
•References
•C.-L. Chang, and R. C.-T. Lee (1997). Symbolic Logic and
Mechanical Theorem Proving. Academic Press.
• J. A.
Robinson(1965). A Machine-Oriented Logic Based on the Resolution Principle.
JACM 12(1): 23-41.
• ロイド,
J.W. (1987). 『論理プログラミングの基礎』佐藤雅彦・森下真一(訳), 産業図書.