7
|
- 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
|
- 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)
|