ノート
スライド ショー
アウトライン
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]と単一化できる。
  • 事実は一つの述語で、ルールは頭部に述語、首記号:-で区切って右側に本体を書く。本体は任意個の述語をカンマで区切って書ける。
  • 本体の条件はカンマで区切られた連言を意味するが、セミコロン;で選言を表せる。例.英語科目:-英文法; 英会話.(⇒英語科目:-英文法.英語科目:- 英会話.のように2つの節に分けても良い。)
  • なおカット!はそれ以降のゴール失敗のとき、バックトラックを!以前まで遡及させない。
  • 矢印‐>は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)は論理学で言う「3段論法」と「背理法」の組合せである。単一化(unification;ユニフィケーション)は、導出を行う際に変数に矛盾のない解を代入すること。背理法ではゴールが正しいことを証明するため、その否定を追加して矛盾を導くことを試みる。 例えば「若者は味噌汁を好まない。」は、xは若者であるをp(x)、味噌汁を好むをq(x)とすると、p(y)→q(y) と書けるだろう。このときもp(a)が正しいなら3段論法によりq(a)を得る。
  • 変数の部分を無視すると、背理法にしたがってp→qという知識の下でqを証明しようとすれば、(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)