論理プログラミング

導出の効率化



ホーン節
ホーン集合に対する導出戦略
論理プログラム


論理式の手続き的解釈
Prolog


カット・オペレータ
閉世界仮説に基づく否定表現
©2008 Ikuo Tahara
1
節の新しい表記法

節: q1 
 qn  p1 
負のリテラル
 (q1 
 (q1 
p1 ,
m 1
 pm
正のリテラル
 qn )  ( p1 
 pm )
 qn )  ( p1 
 pm )
, pm  q1 ,
, qn
ホーン節
©2008 Ikuo Tahara
2
ホーン節(Horn clause)
確定節
p  q1 ,
p
 q1 ,
q1 
 qn  p
p
q1 
 qn
, qn
, qn

ゴール節
©2008 Ikuo Tahara
3
ホーン節に対する導出戦略

SLD(Selective Linear Resolution for Definite Clause)
(1)ゴール節を一方の親節とする.
(2)ゴール節の最左端のリテラルに着目した導出を行う.
 p , r1 ,
, rm
p  q1 ,
 q1 ,
, qn , r1 ,
p  r1 
p  q1 
, qn
, rm
 rm
q1 
 qn  r1 
 qn
 rm
(3)得られたゴール節を次の導出の一方の親節とする.
©2008 Ikuo Tahara
4
SLDは後向き推論である
 A  B, B  C, A
C
後向き推論
ホーン節集合: B  A, C  B, A ,  C
C
B
A

CB
C
肯定式 B  C
BA
A
B
A B
肯定式
A
©2008 Ikuo Tahara
5
論理式の手続き的解釈
p  q1 , q2 ,
p を証明するには
q1 , q2 ,
, qn
, qn を証明すればよい
ホーン節は証明の手続きを表していると解釈できる
p を実行するには,q1 , q2 , , qn を実行すればよい
©2008 Ikuo Tahara
6
論理プログラム

Prolog
頭部(head)
プログラム(確定節)
P  Q1 , Q2 ,
A
本体(body)
, Qn
インタプリタ(SLD導出)
質問(ゴール節)
 G1 , G2 ,
©2008 Ikuo Tahara
, Gm
7
Prologの基本動作

実行の成功
評価(SLD導出)の順序
 G1 , G2 , G3
(1) G1 
成功
(2) G1  Q1 , Q2 , Q3
(3) G1 を直接評価した結果が真
©2008 Ikuo Tahara
8
例
① P  Q, R
P
② QS
③ Q U
 Q, R
④ S
⑤ R
 S, R
R
節の選択は上から下へ

P  Q, R
P
QS
P  Q, R
QS
S
R
S
R
評価は左から右へ
©2008 Ikuo Tahara
9
バックトラックの例
① P  Q, R
P
② Q U
③ QS
 Q, R
④ S
⑤ R
スタック
P  Q, R
Q U
U,R
QS
 Q, R
 S, R
R
失敗
QS
S
R

©2008 Ikuo Tahara
10
実行の失敗とは
① P( x)  Q( x), R( x)
 P( x )
 P( x )
P( x)  Q( x), R( x)
② R ( x)  S ( x)
③ Q( A) 
 Q( x), R( x)
Q( A) 
④ S ( B) 
a. 単一化可能な頭部をもつ節がない.
b. 単一化可能な頭部をもつ節のす
べてが本体の実行に失敗した.
 Q( x), R( x)
 R( A)
R ( x)  S ( x)
 R( A)
 S ( A)
d
b
c. 述語の評価が偽である.
d. バックトラックで再評価したとき別
の選択肢がない.
b
a
©2008 Ikuo Tahara
11
バックトラックの制御
① P  Q,!, R
② PS
③ Q

カット・オペレータ(!)


④ Q U
引数を持たない述語
実行時バックトラック用の選択肢情報を棄却
P
P  Q, !, R
Q, !, R
スタック
PS
Q
©2008 Ikuo Tahara
12
バックトラックの制御
① P  Q,!, R
② PS
③ Q

カット・オペレータ(!)


④ Q U
引数を持たない述語
実行時バックトラック用の選択肢情報を棄却
P
P  Q, !, R
Q, !, R
成功
Q
©2008 Ikuo Tahara
スタック
Q U
PS
13
バックトラックの制御
① P  Q,!, R
② PS
③ Q

カット・オペレータ(!)


④ Q U
引数を持たない述語
実行時バックトラック用の選択肢情報を棄却
P
P  Q, !, R
スタック
Q U
PS
Q, !, R
©2008 Ikuo Tahara
14
バックトラックの制御
① P  Q,!, R
② PS
③ Q

カット・オペレータ(!)


④ Q U
引数を持たない述語
実行時バックトラック用の選択肢情報を棄却
P
P  Q, !, R
スタック
Q, !, R
失敗
©2008 Ikuo Tahara
15
バックトラックの制御
① P  Q,!, R
② PS
③ Q

カット・オペレータ(!)


失敗
④ Q U
引数を持たない述語
実行時バックトラック用の選択肢情報を棄却
P
P  Q, !, R
スタック
Q, !, R
©2008 Ikuo Tahara
16
カット・オペレータを用いた制御構造

条件分岐
if P then Q else R
① if ( P, Q, R)  P, !, Q
② if ( P, Q, R)  R

繰り返し
while P do Q
① while( P, Q)  P, !, Q, while( P, Q)
② while( P, Q) 
©2008 Ikuo Tahara
17
例

好きなものは赤いりんごかみかんである.
りんご?
YES
NO
みかん?
NO
赤い?
YES
① if ( P, Q, R)  P, !, Q
② if ( P, Q, R)  R
NO
YES
好きである
好きでない
likes( x)  if (apple( x), red ( x), orange( x))
©2008 Ikuo Tahara
18
失敗による否定

否定の導入
① not ( P)  P, !, FAIL
② not ( P) 
成功
not ( P)は失敗
P である
失敗
not ( P)は成功
P でない
P の実行
©2008 Ikuo Tahara
19
閉世界仮説

失敗による否定は閉世界仮説に基づく
 not ( A)
not ( P)  P, !, FAIL
 A, !, FAIL
 not ( A)
not ( P) 
A
B
失敗

B
真なる事柄は
すべて表示されている
閉世界仮説
©2008 Ikuo Tahara
20
失敗による否定  論理的否定
 P( x)
 not ( P( x))
誤解
質問: xQ( x)
「P(x) の実行に失敗する」?
(xQ( x))
 x[Q( x)]
「P である x は存在しない」?
ゴール節:  Q( x)
x[P( x)] ?
x[P( x)] ?
©2008 Ikuo Tahara
21
例
太郎が嫌いなものは何か?
① likes (Taro, Apple) 
 not (likes(Taro, x))
② fruit ( Apple) 
③ fruit ( Peach) 
not ( P)  P, !, FAIL
失敗
好きなものがある
 likes(Taro, x), !, FAIL
太郎は嫌いなものはない(すべて好き)
likes(Taro, Apple) 
?
太郎は桃が嫌い(閉世界仮説より)
誤解を招かない質問
 fruit ( x), not (likes(Taro, x))
 !, FAIL
失敗
©2008 Ikuo Tahara
22
ダウンロード

論理プログラミング