導出原理と導出戦略

導出原理の適用




一般の節集合に対する導出原理
最汎単一化置換
論理による問題解決
導出の制御戦略


横形優先戦略
線形導出
©2008 Ikuo Tahara
1
基礎節の集合に対する導出原理
S  { p( x), p(a)  q( f ( y)), q( z )}
エルブランの定理
S *  { p(a), p( f (a)),
, p(a)  q( f (a)),
, q(a), q( f (a)), }
q( f (a))
導出原理
©2008 Ikuo Tahara
2
単一化(unification)
{ , p( x, f ( y))  q( x),
, p(a, z )  r ( z ), }
xa
z  f ( y)
p(a, f ( y ))  q(a)
p(a, f ( y))  r ( f ( y))
q(a)  r ( f ( y ))
©2008 Ikuo Tahara
3
最汎単一化置換
p ( x, a, f ( z ))
p ( g ( y ), y , w)
©2008 Ikuo Tahara
4
最汎単一化置換
p ( x, a, f ( z ))
D  {x, g ( y )}
p ( g ( y ), y , w)
x  g ( y)
©2008 Ikuo Tahara
5
最汎単一化置換
p ( g ( y ), a, f ( z ))
D  {x, g ( y )}
p ( g ( y ), y, w)
x  g ( y)
©2008 Ikuo Tahara
6
最汎単一化置換
p ( g ( y ), a, f ( z ))
D  {a, y}
p ( g ( y ), y, w)
ya
©2008 Ikuo Tahara
7
最汎単一化置換
p( g (a ), a, f ( z ))
D  {a, y}
p( g (a ), a, w)
ya
©2008 Ikuo Tahara
8
最汎単一化置換
p( g (a ), a, f ( z ))
D  { f ( z ), w}
p( g (a ), a, w)
w  f ( z)
©2008 Ikuo Tahara
9
最汎単一化置換
p( g (a ), a, f ( z ))
D  { f ( z ), w}
p( g (a ), a, f ( z ))
w  f ( z)
©2008 Ikuo Tahara
10
最汎単一化置換
p( g (a ), a, f ( z ))
D
p( g (a ), a, f ( z ))
{x  g ( y )} { y  a} {w  f ( z )}
 {x  g (a), y  a, w  f ( z )}
©2008 Ikuo Tahara
11
論理による問題解決
太郎は花子の父である.
次郎は太郎の父である.
花子の祖父は誰か?
父の父は祖父である.
F (Taro, Hanako)
F ( Jiro, Taro)
xyz.[ F ( x, y )  F ( y, z )  G ( x, z )]
©2008 Ikuo Tahara
w.G( w, Hanako)
12
論理による問題解決
① F (Taro, Hanako)
② F ( Jiro, Taro)
③ xyz.[ F ( x, y )  F ( y, z )  G ( x, z )]
④ w.G( w, Hanako)
①  ②  ③  ④
 F (Taro, Hanako),

 F ( Jiro, Taro),



S 

F ( x, y )  F ( y, z )  G ( x, z ), 


G ( w, Hanako)

©2008 Ikuo Tahara
13
論理による問題解決
F ( Jiro, Taro)
F (Taro, Hanako)
F ( x, y )  F ( y, z )  G ( x, z ) G ( w, Hanako)
w x
F ( x, y )  F ( y, Hanako)
x  Jiro
F ( x, Taro)
z  Hanako
y  Taro
{w  x} {x  Jiro}
 {w  Jiro, x  Jiro}
©2008 Ikuo Tahara
14
導出の制御戦略

基本的な制御戦略



横形優先戦略(breadth-first strategy)
線形導出(linear resolution)
意味に基づく制御戦略


支持集合戦略(set-of-support strategy)
意味導出(semantic resolution)
©2008 Ikuo Tahara
15
横形優先戦略
節集合
第1段階の導出
第2段階の導出
©2008 Ikuo Tahara
16
例
p( x)  q( x) q( y)  r ( y) r ( z )  s( z )
q(a)
r (a)
p( w1 )  r ( w1 )
s(a)
p(a) s (a )
q( w2 )  s( w2 )
p( w3 )  s( w3 )
©2008 Ikuo Tahara
q(a)
r (a)
p(a)
17
線形導出
節集合
©2008 Ikuo Tahara
18
例
p( x)  q( x) q( y)  r ( y) r ( z )  q( z )
p(a)
q(a)
r (a)
q(a)
©2008 Ikuo Tahara
19
支持集合戦略

 
充足不能
からの節集合   からの節集合
支持集合
充足可能
©2008 Ikuo Tahara
20
例
{ p  q  r , p  q, p} q  r
{ p  q  r , p  q, p, q  r }
支持集合
p  q
p
©2008 Ikuo Tahara
21
意味導出

一つの解釈 I を設定する.
導出節も含む節の集合
解釈Iで真となる
節の集合
解釈Iで偽となる
節の集合
©2008 Ikuo Tahara
22
例
{p  q, q  r , p, r  s, s}
I  { p  F, q  T, r  T, s  F}
q r, p, s
p  q, r  s
p r
r
s
©2008 Ikuo Tahara
23
順序付き線形導出(OL導出)



節におけるリテラルの並び順を固定する.
最右リテラルに着目し,それと相補的なリテラル
を持つ節を選び導出を行う.
着目したリテラルを四角で囲い導出節に残す.
l1 
l1 
 ln  l
l1 
 ln  l  l1 
 lk   l  lk1 
 lk  lk1 
©2008 Ikuo Tahara
 lm
 lm
24
導出節に対する処理(1)

l1 
縮約(reduction)
 ln  l  l1
Pl
 lm   l
l  Q
PQ
l1 
 ln  l  l1
この処理の結果 l1 
となれば l1 
 lm
 ln  l
 ln とする.
©2008 Ikuo Tahara
P  l
P
25
導出節に対する処理(2)

簡約(factorization)
l1 
 p
 ln  l  l1
 p
l1 
 p
 ln  l  l1
 lm
この処理の結果 l1 
となれば l1 
 p
 p
 lm
 ln  l
 ln とする.
©2008 Ikuo Tahara
26
{ p  q, q  r, q  r , r  p, p  r}
pqr
p  q  r  q
pq
pqr
pr
p
q  r q  r
p  q
pr
p
p  r  p
27
ダウンロード

導出原理と導出戦略