1	Prologによる論理プログラミング
2	Prologの例1（知識ベース）
3	Prologの例2（問題解決システム）
4	Prologの例3（集合論的操作）
5	Prologの例4（合理的選択）
6	Prologの例5（ナッシュ均衡）
7	付録A．Prologの構文、リスト、節など Prologでは述語を述語名とカッコで表し、カッコ内には引数を任意個数カンマで区切って設定できる。引数には個体記号、変数、リスト形式を使用できる。個体記号：　小文字で始める文字列。あるいは数字。その他の文字列は引用符‘’で囲えばよい。また「親（親（X))」（＝Xの祖父）のように変数を含んだ関数の使用も許される。変数：　英大文字で始める。下線_で始めれば無名変数。リスト形式：　任意個のアトムの列）も使える。たとえば[a,b,c,d]はリストだが、左端と残りのペアを縦棒で区切って[a\|Y] 、Y=[b,c,d]と単一化できる。事実は一つの述語で、ルールは頭部に述語、首記号:-で区切って右側に本体を書く。本体は任意個の述語をカンマで区切って書ける。本体の条件はカンマで区切られた連言を意味するが、セミコロン；で選言を表せる。例．英語科目:-英文法; 英会話.（⇒英語科目:-英文法.英語科目:- 英会話.のように２つの節に分けても良い。）なおカット！はそれ以降のゴール失敗のとき、バックトラックを！以前まで遡及させない。矢印‐>はIf-Then文として使える。節形式はリテラルの選言（「または」を意味する論理結合子（∨）で結ばれたリテラルの列）である。ホーン節(Horn clause)は肯定リテラルが一つだけ許されている節形式であり、以下のような冠頭標準形に対応する。リテラルは引数を特定した述語と考えてよいが、否定(\+)がつく場合を含む。ルール節 p(x):- q(x), r(x). の宣言的意味は「もしxがqとrという条件を同時に満たしているならば、pという条件も満たすはずである。」という主張に等しい。論理式では、 q∧r → p あるいはp∨ not q∨ not r という形式で表せる（ただし全称∀が全体につくので唯一の変数xは省略した）。 ∧（連言）、∨（選言）、not（否定）、→（条件）は標準的な論理学の約束にしたがう。
8	付録B．Prologによる自動証明（導出と単一化） 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). 『論理プログラミングの基礎』佐藤雅彦・森下真一(訳), 産業図書. Wielemaker, J. (1994). SWI-Prolog 1.6 Reference Manual. In Kantrowitz(ed.), CMU AI Repository. Prime Time Freeware for AI, Issue 1-1. (software with manual is downloadable from URL http://www-2.cs.cmu.edu/afs/cs/project/ai-repository/ai/lang/prolog/impl/prolog/swi_pl/0.html)