情報実習II

数理論理学
第13回
導出原理2
(mguと導出原理)
© 加藤，高田，新出
4.2.2項(p. 96)
mgu
4.2.3項(p. 97)
導出原理を用い
た推論手順
4.2.1 導出原理の概要 (p. 90)
(前回の復習)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
{sumire/x, maruko/y}
mother(sumire,maruko)∨￢parent(sumire,maruko)
∨￢female(sumire)
￢
mother(sumire,maruko)
￢parent(sumire,maruko)∨￢female(sumire)
節4.3 と 4.4 の導出節 (p. 90 ll. 4)
4.2.1 導出原理の概要 (p. 91)
(前回の復習)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
￢parent(sumire,maruko)∨￢female(sumire)
￢female(sumire)
三段論法
p. 92, p. 41
(空節) mgu {sumire/x, maruko/y}
4.2.2 単一化と mgu (pp. 94, 95)
(前回の復習)
定義 4.9 単一化アルゴリズム
例 4.11 S={mother(x,y) , mother(w,maruko)}
・ S0 ={mother(x,y) , mother(w,maruko)}
θ0=ε ={}
・ D0 ={x,w} x0=x, t0=w
S の単一化代入
・ θ1=θ0 ○{w/x}= {w/x}
S1 =S0θ1 ={mother(w,y), mother(w,maruko)}
・ D1 ={y,maruko} x1=y, t1=maruko
・ θ2=θ1 ○{maruko/y}= {w/x, maruko/y}
S2 =S1θ2 ={mother(w,maruko), mother(w,maruko)}
={mother(w,maruko)}
(p. 1 参照)
課題12 下記の S を単一化せよ
全て記述
S ={parent(hiroshi,y) , parent(v,z)} すること
・ S0 ={parent(hiroshi,y) , parent(v,z)}
θ0=ε ={}
・ D0 ={
・ θ1=θ0 ○{
S1 =S0θ1 ={
・ D1 ={
・ θ2=θ1 ○{
S2 =S1θ2 ={
} x0= ,
} ={
t0=
}
}
} x1= , t1=
}= {
={parent(hiroshi,z)}
}
}
課題12 下記の S を単一化せよ
全て記述
S ={parent(hiroshi,y) , parent(v,z)} すること
・ S0 ={parent(hiroshi,y) , parent(v,z)}
θ0=ε ={}
・ D0 ={hiroshi, v} x0=v, t0=hiroshi
・ θ1=θ0 ○{hiroshi/v}= {hiroshi/v}
S1 =S0θ1 ={parent(hiroshi,y), parent(hiroshi,z)}
・ D1 ={y,z} x1=y, t1=z
・ θ2=θ1 ○{z/y}= {hiroshi/v , z/y}
S2 =S1θ2 ={parent(hiroshi,z), parent(hiroshi,z)}
={parent(hiroshi,z)}
4.2 導出原理による推論
(p. 92)
4.2.1 導出原理の概要
4.2.2 単一化とmgu
• 単一化代入
• 不一致集合
• 代入の合成
• 単一化アルゴリズム
• mgu
4.2.3 導出原理を用いた推論手順
4.2 導出原理による推論
(p. 92)
4.2.1 導出原理の概要
4.2.2 単一化とmgu
• 単一化代入
• 不一致集合
• 代入の合成
• 単一化アルゴリズム
• mgu
4.2.3 導出原理を用いた推論手順
4.2.2 単一化と mgu (p. 93)
(前回の復習)
定義 4.8 代入の合成 σ○θ
任意の項または論理式 F に対して
(F θ2)σ= F θ1 : θ1はθ2とσの合成
σ
θ
2
例 4.10
○
θ1 ={sumire/x, maruko/y, sumire/w}
θ2 ={w/x, maruko/y},
σ ={sumire/w}
mother(x,y) θ1 =mother(sumire,maruko)
mother(x,y) θ2 =mother(w,maruko)
mother(w,maruko)σ =mother(sumire,maruko)
4.2.2 単一化と mgu (p. 96)
定義 4.10 代入間の等価性
任意の項または論理式 F に対して
F θ1= F θ2 θ1＝θ2
例 4.10 θ1＝ σ θ2
○
θ1 ={sumire/x, maruko/y, sumire/w}
θ2 ={w/x, maruko/y},
σ ={sumire/w}
mother(x,y) θ1 =mother(sumire,maruko)
mother(x,y) θ2 =mother(w,maruko)
mother(w,maruko)σ =mother(sumire,maruko)
4.2.2 単一化と mgu (p. 96)
定義 4.11 最汎単一化代入 mgu
ある σ に対して θ1＝ σ ○ θ2 となるとき
より一般的
θ2 は θ1 に対してより一般的である
代入の結果より多くの変数が残る
例 4.13 {mother(x,y) , mother(w,maruko)}
θ1 ={sumire/x, maruko/y, sumire/w}
(ll.6)
θ2 ={w/x, maruko/y},
σ1 ={sumire/w}
mother(x,y) θ1 =mother(sumire,maruko)
mother(x,y) θ2 =mother(w,maruko)
mother(w,maruko)σ1=mother(sumire,maruko)
より多くの
4.2.2 単一化と mgu (p. 96)
変数が残る
定義 4.11 最汎単一化代入単一化 (p. 96 ll. 6)
例 4.12-13{mother(x,y) , mother(w,maruko)}
θ1 ={sumire/x, maruko/y, sumire/w}
θ2 ={w/x, maruko/y}
θ3 ={hiroshi/x, maruko/y, hiroshi/w}
σ1 ={sumire/w}, σ2 ={hiroshi/w}
mother(x,y) θ1 =mother(sumire,maruko)
mother(x,y) θ2 =mother(w,maruko)
θ1＝ σ1 θ2
○
θ 3＝ σ2 θ 2
○
mother(x,y) θ3 =mother(hiroshi,maruko)
4.2.3 導出原理を用いた推論手順 (pp. 97-98)
定義 4.12 導出原理 S  {C1 , C2 ,, Cm }
条件1.
条件2.
4.2.3 導出原理を用いた推論手順 (pp. 97-98)
定義 4.12 導出原理 S  {C1 , C2 ,, Cm }
条件1. C1 とC2に共通する変数は存在しない
p. 102 例4.18
{ female(sumire),
(4.14)
parent(sumire,maruko),
(4.15)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(w,maruko) }
(4.17)
(4.16)
C1 とC2 から導出節が得られるはずなのに、得られ
なくなってしまうから（詳しくはp. 99 例4.14参照）
4.2.3 導出原理を用いた推論手順 (pp. 97-98)
定義 4.12 導出原理 S  {C1 , C2 ,, Cm }
条件2. C1 とC2 の単一化可能なリテラルの指定
k 1
1
C1  L  L    L  L
1
1
2
1
k
1
m 1
2
C2  L  L    L  L
1
2
2
2
m
2
 L
l
1
  L
n
2
{ female(sumire),
(4.14)
parent(sumire,maruko),
(4.15)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(w,maruko) }
(4.17)
(4.16)
4.2.3 導出原理を用いた推論手順 (pp. 97-98)
定義 4.12 導出原理 S  {C1 , C2 ,, Cm }
条件2. C1 とC2 の単一化可能なリテラルの指定
k 1
1
C1  L  L    L  L
1
1
2
1
k
1
m 1
2
C2  L  L    L  L
1
2
2
2
k 1
1
Cr  L
m
2
m1
2
  L  L
l
1
 L
l
1
  L
n
2
  L
n
2
一般にはこのような導出節は複数存在
Cr1 , Cr12 , Cr13 ,
4.2.3 導出原理を用いた推論手順 (pp. 97-98)
定義 4.13 導出R( ) S  {C1 , C2 ,, Cm }
R( S )  S  {
Cr | C1  S , C2  S , Crは
C1とC2の導出節}
一般にはこのような導出節は複数存在
Cr1 , Cr12 , Cr13 ,
R( S )
 {C1 , C2 , , Cm , Cr1 , Cr1 2 , Cr13 , }
例 4.16 (pp. 100-101)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
{sumire/x, maruko/y}
mother(sumire,maruko)∨￢parent(sumire,maruko)
∨￢female(sumire)
￢
mother(sumire,maruko)
￢parent(sumire,maruko)∨￢female(sumire)=Cr1
例 4.16 (p. 101)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
{sumire/x, maruko/y}
female(sumire)
mother(sumire,maruko)∨￢parent(sumire,maruko)
∨￢female(sumire)
mother(sumire,maruko)∨￢parent(sumire,maruko)
=Cr1-2
式 (4.12)
例 4.16 (p. 101)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
{sumire/x, maruko/y}
parent(sumire,maruko)
mother(sumire,maruko)∨￢parent(sumire,maruko)
∨￢female(sumire)
mother(sumire,maruko)∨￢female(sumire) =Cr1-3
式 (4.13)
例 4.16 (pp. 100-101)
R(S )  {C1 , C2 ,, Cm , Cr1 , Cr12 , Cr13}
R(S)=
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko)
(4.4)
￢parent(sumire,maruko)∨￢female(sumire)
mother(sumire,maruko)∨￢parent(sumire,maruko)
mother(sumire,maruko)∨￢female(sumire) }
(4.3)
4.2.3 導出原理を用いた推論手順 (pp. 97-98)
n
定義 4.14 第n導出 R (S)
R (S )  S ,
0
R ( S )  R( S ), R ( S )  R ( R( S ))
1
R
2
n 1
( S )  R ( R ( S ))
n
n
定義 4.14 第n導出 R (S)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
mother(sumire,maruko)∨￢parent(sumire,maruko)
∨￢female(sumire)
￢
mother(sumire,maruko)
￢parent(sumire,maruko)∨￢female(sumire)=Cr1
第1導出
R(S )  {C1 , C2 ,, Cm , Cr1 , Cr12 , Cr13}
n
定義 4.14 第n導出 R (S)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
￢parent(sumire,maruko)∨￢female(sumire)
￢female(sumire)
第2導出
(空節)
第3導出
例 4.18 mgu が必要な理由 (p. 103 l.1 しかし～)
{ female(sumire),
(4.14)
parent(sumire,maruko),
(4.15)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(w,maruko) }
(4.17)
(4.16)
θ3 ={ maruko/x, maruko/w, maruko/y}
mother(maruko,maruko)∨￢parent(maruko,maruko)
∨￢female(maruko)
￢
mother(maruko,maruko)
￢parent(maruko,maruko)∨￢female(maruko)
これ以上の導出は無理
例 4.18 mgu が必要な理由 (pp. 103 しかし)
{ female(sumire),
(4.14)
parent(sumire,maruko),
(4.15)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(w,maruko),
(4.17)
female(maruko) なら}
￢parent(maruko,maruko)∨￢female(maruko)
(4.16)
female(maruko)
￢parent(maruko,maruko)
それでもこれ以上の導出は無理
例 4.18 mgu が必要な理由 (pp. 103 しかし)
{ female(sumire),
(4.14)
parent(sumire,maruko),
(4.15)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(w,maruko) }
(4.17)
(4.16)
θ3 ={ maruko/x, maruko/w, maruko/y}
mguでないことが原因
(ll. 10)
mother(maruko,maruko)
∨￢parent(maruko,maruko)
∨￢female(maruko)
￢
mother(maruko,maruko)
￢parent(maruko,maruko)∨￢female(maruko)
例 4.18 mgu が必要な理由 (pp. 103 しかし)
{ female(sumire),
(4.14)
parent(sumire,maruko),
(4.15)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(w,maruko) }
(4.17)
(4.16)
mother(w,maruko)∨￢parent(w,maruko)∨￢female(w)
θ2 ={ w/x, maruko/y}
￢ mother(w,maruko)
￢parent(w,maruko) σ∨￢female(w) σ σ ={sumire/w}
(p. 104)
￢female(sumire) 変数に具体的な値を
(空節)
入れるタイミングは
できるだけ後にする(p. 103 ll. 5)
課題13 節集合S に対する導出演繹を行え
S={ parent(hiroshi, sakiko),
child(x, y) ∨￢parent(y, x),
￢ child(sakiko,w)
}
(1)
(2)
(3)
節 (2) と (3)を用いて導出を行う。このとき
のmgu は{w
/ y}.
{ /x, hiroshi/x,
/ y}. (a)
このmgu を節(2)と(3)に適用すると、以下のようになる。
(b)
child(w, hiroshi) ∨￢parent(hiroshi,w)
￢ child(w, hiroshi)
(c)
導出の結果、次の二項導出節 (d) が残る。
￢parent(w, sakiko).
これと、節 (1) から導出を行う。 mgu は
(e) 節(1)を使って導出を進める。
{sakiko/w}.
￢parent(hiroshi , sakiko)
(f)
parent(hiroshi , sakiko)
(g)
□
導出の結果、空節(h) が求まる。

Download Report