情報実習II

数理論理学
第14回
導出原理の健全性と完全性
エルブランの定理
© 加藤，高田，新出
4.3節(p. 104)
導出原理の健全
性と完全性
課題13 節集合S に対する導出原理を行え
S={ parent(hiroshi, sakiko),
child(x, y) ∨￢parent(y,x),
￢ child(sakiko,w)
}
(1)
(2)
(3)
節 (2) と (3)を用いて導出を行う。このとき
のmgu は{w/y, sakiko/x}.
(a)
このmgu を節(2)と(3)に適用すると、以下のようになる。
child(sakiko, w) ∨￢parent(w,sakiko) (b)
￢ child(sakiko,w)
(c)
導出の結果、次の導出節 (d) が残る。
￢parent(w, sakiko).
これと、節 (1) から導出を行う。 mgu は
節(1)を使って導出を進める。
{hiroshi/w}. (e)
￢parent(hiroshi , sakiko)
(f)
parent(hiroshi , sakiko)
(g)
□
導出の結果、空節 (h) が求まる。
導出原理の健全性 (p. 104)
節集合 S から導出原理によって空節を
得れば， S は充足不能(p. 65) である。
{ parent(hiroshi, maruko)
child(x, y) ∨￢parent(y, x)
￢ child(maruko, w) }
導出原理
3.2.2 解釈
定義 3.17
論理式や、関数に意味を
与えるもの。 (p. 61)
解釈
I ( D,A )
対象領域割り当て
定義3.14
定義3.15
Dの例
D  {tom ozou, kotake, hiroshi, sum ire,
sakiko, m aruko}
割り当て
述語記号に対しては、 D  {, T}
m
の関数を割り当てる。
Aの例 : D  {tom ozou, kotake,}, m  2
A ( parent)(tom ozou, hiroshi)  T (真)
A ( parent)(tom ozou, m aruko)  (偽)

割り当て
関数記号に対しては、関数
D　 D を割り当てる。
m
D  {tom ozou, kotake, hiroshi}
A (elder)(tom ozou, hiroshi)  tom ozou
A (elder)(m aruko, sakiko)  sakiko

さくら家における解釈を I ( D ,A )
sakura
sakura
とする。ただし
Dsakura  {tomozou, kotake, hiroshi, sumire, sakiko, maruko}
Asakura とは、さくら家における述語記号や関数記号の割り当て
Asakura ( parent) 表
tomozou
kotake
hiroshi
…
maruko
tomozou
⊥
⊥
T
…
⊥
kotake
⊥
⊥
T
…
⊥
hiroshi
⊥
⊥
⊥
…
T
…
…
…
…
…
…
maruko
⊥
⊥
⊥
…
⊥
さくら家における解釈を I ( D ,A )
sakura
sakura
とする。ただし
Dsakura  {tomozou, kotake, hiroshi, sumire, sakiko, maruko}
Asakura とは、さくら家における述語記号や関数記号の割り当て
Asakura (elder) 表
hiroshi
…
maruko
tomozou tomozou tomozou tomozou
…
tomozou
tomozou
kotake
kotake
tomozou
kotake
kotake
…
kotake
hiroshi
tomozou
kotake
hiroshi
…
hiroshi
…
…
…
…
…
…
maruko
tomozou
kotake
hiroshi
…
maruko
導出原理の健全性 (p. 104)
節集合 S から導出原理によって空節を
得れば， S は充足不能(p. 65) である
{ parent(hiroshi, maruko)
child(x, y) ∨￢parent(y, x)
￢ child(maruko, w) }
I1
I2
導出原理
Im
どんな解釈を持ってきても、S のモデルにはならない
導出原理の完全性 (p. 104)
充足不能な節集合 S に対して導出原理
により必ず空節を得る
{ parent(hiroshi, maruko)
child(x, y) ∨￢parent(y, x)
S2
S1
￢ child(maruko, w) }
導出原理
S3
Sn
S4
I1
I2
Im
どんな解釈を持ってきても、S のモデルにはならない
モデルによる充足不能判定
導出原理による充足不能判定
どんな解釈
導出原理によって
I を使っても
空節が得られる
I(S)= ⊥
定理4.4 導出原理の健全性と完全性 (p. 104)
エルブランの定理 (p. 110 定理 4.3)
どんな解釈、つまり無限にあるあらゆる
定義4.16 エルブラン領域 (p. 105)
解釈を扱い証明することは困難
定義4.17 エルブラン基底 (p. 105)
定義4.18 割り当てAS (p. 105)
定義4.19 エルブラン解釈とエルブランモデル(p. 107)
モデルによる充足不能判定
導出原理による充足不能判定
どんな解釈
導出原理によって
I を使っても
空節が得られる
I(S)= ⊥
定理4.4 導出原理の健全性と完全性 (p. 104)
エルブランの定理 (p. 110 定理 4.3)
定義4.16
定義4.17
定義4.18
定義4.19
エルブラン領域 (p. 105)
エルブラン基底 (p. 105)
割り当てAS (p. 105)
エルブラン解釈とエルブランモデル(p. 107)
定義4.16 エルブラン領域HUS (p. 105)
(空集合)
Constants(S) (Constants(S) ≠ ∅)
HU0=
{a}
(Constants(S) = ∅)
S=
例4.19 (p. 106) (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)
HU0={sumire,maruko} = HUS
(S に関数記号が
ないので (p. 106 l.4) )
定義4.16 エルブラン領域HUS (p. 105)
Constants(S) (Constants(S) ≠ ∅)
HU0=
{a}
(Constants(S) = ∅)
S 内に関数記号がある場合
HUi+1= HUi ∪{f(t1,…,tn) | ・・・・・・・・・}
HUS =∪
HU
i
i ∈ω
定義4.16 エルブラン領域HUS (p. 105)
S
例4.20
(pp.
106-107)
{ sum(0, x, x),
￢sum(x, y, z)∨sum(succ(x), y, succ(z))}
HU0
HU1
HU2
HU3
= {0}
HUs
= {0, succ(0)}
= {0, succ(0), succ(s(0))}
= {0, succ(0), succ(succ(0)), …}
：
HUi+1 = {0, succ(0), succ(succ(0)),
i
：
…, succ(succ (0))}
定義4.16 エルブラン領域HUS (p. 105)
(空集合)
Constants(S) (Constants(S) ≠ ∅)
HU0=
{a}
(Constants(S) = ∅)
S=
例4.19 (p. 106) (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)
HU0={sumire,maruko} = HUS
(S に関数記号が
ないので (p. 106 l.4) )
モデルによる充足不能判定
導出原理による充足不能判定
どんな解釈
導出原理によって
I を使っても
空節が得られる
I(S)= ⊥
定理4.4 導出原理の健全性と完全性 (p. 104)
エルブランの定理 (p. 110 定理 4.3)
定義4.16
定義4.17
定義4.18
定義4.19
エルブラン領域 (p. 105)
エルブラン基底 (p. 105)
割り当てAS (p. 105)
エルブラン解釈とエルブランモデル(p. 107)
定義4.17 エルブラン基底 (p. 105)
HBS = {p(t1,…,tm) | p は S に現れるarity m
の述語記号, t1,…,tm ∈ HUS }
S=
例4.19 (p. 106) (p. 90)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
HUS={sumire,maruko}
HBS={female(sumire), female(maruko), …
(4.3)
定義4.17 エルブラン基底 (p. 105)
例4.19 (p. 106) (p. 90)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
HUS={sumire,maruko}
HBS={female(sumire), female(maruko),
(4.3)
parent(sumire,sumire), parent(sumire, maruko),
parent(maruko,sumire), parent(maruko, maruko),
mother(sumire,sumire),mother(sumire,maruko),
mother(maruko,sumire),mother(maruko,maruko)}
定義4.17 エルブラン基底
例4.20
(pp. 106-107)
{ sum(0, x, x),
S
￢ sum(x, y, z) ∨ sum(succ(x), y, succ(z))}
HUs = {0, succ(0), succ(succ(0)), HUs
…, succ(succ i(0))}
HBS = {sum(0, 0, 0), sum(0, 0, succ(0)),
2
3
…, sum(succ(0), succ (0), succ (),
…}
モデルによる充足不能判定
導出原理による充足不能判定
どんな解釈
導出原理によって
I を使っても
空節が得られる
I(S)= ⊥
定理4.4 導出原理の健全性と完全性 (p. 104)
エルブランの定理 (p. 110 定理 4.3)
定義4.16
定義4.17
定義4.18
定義4.19
エルブラン領域 (p. 105)
エルブラン基底 (p. 105)
割り当てAS (p. 105)
エルブラン解釈とエルブランモデル(p. 107)
定義4.18 割り当てAS
(p. 105)
Dsakura  {tomozou, kotake, hiroshi, sumire, sakiko, maruko}
Asakura とは、さくら家における述語記号や関数記号の割り当て
Asakura ( parent) 表
tomozou
kotake
hiroshi
…
maruko
tomozou
⊥
⊥
T
…
⊥
kotake
⊥
⊥
T
…
⊥
hiroshi
⊥
⊥
⊥
以前の割り当て
…
… (pp. 56-59)
…
定義3.15
…
T
…
…
⊥
…
⊥
…
maruko
⊥
⊥
定義4.18 割り当てAS (p. 105)
AS は HBS の部分集合 (AS ⊆ HBS)
(定義のl.2)
真偽の求め方
AS（L) =
T
⊥
(L∈
AS の場合 )
(その他の場合 )
例4.19 (p. 106)
HBS={female(sumire), female(maruko),
parent(sumire,sumire), parent(sumire, maruko),
parent(maruko,sumire), parent(maruko, maruko),
mother(sumire,sumire),mother(sumire,maruko),
mother(maruko,sumire),mother(maruko,maruko)}
maruko),
AS ={parent(sumire,
female(sumire), mother(sumire,maruko)}
(p. 106 ll. 7)
真偽の求め方
AS（L) =
T
⊥
(L∈
AS の場合 )
例4.19 (p. 106)
HBS={female(sumire), female(maruko),
(その他の場合 )
parent(sumire,sumire), parent(sumire, maruko),
parent(maruko,sumire), parent(maruko, maruko),
mother(sumire,sumire),mother(sumire,maruko),
mother(maruko,sumire),mother(maruko,maruko)}
maruko),
AS ={parent(sumire,
female(sumire), mother(sumire,maruko)}
ASSS（female(sumire))
（mother(sumire,maruko))
== TT
（parent(sumire, maruko))
=T
AS（parent(maruko, maruko)) =⊥
(p.
(p.106
106 ll.
ll.5)
6)
モデルによる充足不能判定
導出原理による充足不能判定
どんな解釈
導出原理によって
I を使っても
空節が得られる
I(S)= ⊥
定理4.4 導出原理の健全性と完全性 (p. 104)
エルブランの定理 (p. 110 定理 4.3)
定義4.16
定義4.17
定義4.18
定義4.19
エルブラン領域 (p. 105)
エルブラン基底 (p. 105)
割り当てAS (p. 105)
エルブラン解釈とエルブランモデル(p. 107)
3.2.2 解釈
以前の解釈 (pp. 61-65)
定義 3.17
解釈
I ( D,A )
対象領域割り当て
定義3.14
定義3.15
Dの例
D  {tom ozou, kotake, hiroshi, sum ire,
sakiko, m aruko}
定義4.18 割り当てAS
(p. 105)
Dsakura  {tomozou, kotake, hiroshi, sumire, sakiko, maruko}
Asakura とは、さくら家における述語記号や関数記号の割り当て
Asakura ( parent) 表
tomozou
kotake
hiroshi
…
maruko
tomozou
⊥
⊥
T
…
⊥
kotake
⊥
⊥
T
…
⊥
hiroshi
⊥
…
maruko
…
⊥
⊥
以前の領域と割り当て
…
… (pp. 56-59)
…
…
定義3.15
…
⊥
⊥
⊥
⊥
…
T
定義4.19 エルブラン解釈と
エルブランモデル (p. 107)
エルブラン解釈
HI( HU S ,AS )
エルブラン領域
割り当て
S={ bird(hawk), bird(eagle), 例4.21 (p. 107)
fly(x) ∨ ￢ bird(x) }
HUs = {hawk, eagle}
HBS = {bird(hawk), bird(eagle),
fly(hawk), fly(eagle)}
1
2
AS  ∅ AS ={bird(hawk)} AS3 ={fly(eagle)}
… AS5 ={bird(hawk), bird(eagle)}
16
… AS = HBS
(p. 108)
S={ bird(hawk),C1 bird(eagle),C2 例4.21
p. 109 の箇条書
fly(x) ∨ ￢ bird(x) C3 }
HUs = {hawk, eagle}
AS =HBS = {bird(hawk), bird(eagle),
fly(hawk), fly(eagle)}
HI  HI( HU S ,AS )とする。HI(S)=Tとなることを示すため
・ HI({bird(hawk)})=HI({bird(eagle)})=
HI({fly(x) ∨ ￢ bird(x) })=Tを示す (p. 109 l. 6)
・ bird(hawk), bird(eagle)∈AS より、
HI({bird(hawk)})=HI({bird(eagle)})= T(l. 10)
・ HI({fly(x) θ∨ ￢ bird(x) θ })=T ?
(l. 8)
(p. 108)
S={ bird(hawk),C1 bird(eagle),C2 例4.21
p. 109 の箇条書
fly(x) ∨ ￢ bird(x) C3 }
HUs = {hawk, eagle}
AS =HBS = {bird(hawk), bird(eagle),
fly(hawk), fly(eagle)}
・ HI({fly(x) θ∨ ￢ bird(x) θ })=T ?
・ θ ={hawk/x}のとき
(l. 8)
HI({fly(hawk) ∨ ￢ bird(hawk) }= T
・ θ ={eagle/x}のとき
HI({fly(eagle) ∨ ￢ bird(eagle) }= T
以上より、HI は S のエルブランモデル
定理 4.2 (p. 110)
節集合 S が充足不能性である
iff (必要十分条件)
S のエルブランモデルが存在しない
定理 4.3 (p. 110)
節集合Sが充足不能
iff
Sの基礎節集合GCS のある有限集合が
充足不能である。
定義 4.20 基礎節集合 GCS
S={ bird(hawk),
bird(eagle),
fly(x) ∨ ￢ bird(x)
(p. 109)
例4.22(p. 109)
}
HUs = {hawk, eagle}
GCS ={ bird(hawk),
bird(eagle),
fly(hawk) ∨ ￢ bird(hawk),
fly(eagle) ∨ ￢ bird(eagle) }
S=
{parent(hiroshi,maruko),
C1
male(hiroshi),
C2
father(x,y)∨￢parent(x,y)∨￢male(x) C3}
} を節集合とする。
課題14-1 S に対するエルブラン基底
(要素10個)を求めよ。
課題14-2 S に対するエルブラン解釈
HI = {parent(hiroshi,maruko), male(hiroshi), father(hiroshi, maruko)}.
がエルブランモデルであることを証明せよ。
S={parent(hiroshi,maruko),
C1 解答
male(hiroshi),
C2
father(x,y)∨￢parent(x,y)∨￢male(x) C3}
HUs = {hiroshi, maruko}
HBS =
{
parent(hiroshi,hiroshi),parent(hiroshi,maruko),
parent(maruko,hiroshi), parent(maruko,maruko),
male(hiroshi), male(maruko),
father(hiroshi,hiroshi),father(hiroshi,maruko),
father(maruko,hiroshi), father(maruko,maruko)
}
Sの一つのエルブラン解釈 HI を以下のように取るとき、
HI = {parent(hiroshi,maruko), male(hiroshi), father(hiroshi, maruko)}.
この HI が S のエルブランモデルであることを証明する。
parent(hiroshi,maruko)∈HI より、
HI({parent(hiroshi,maruko)})= T 。
同様に、 HI (male(hiroshi))= T 。
次に、節C3= father(x,y)∨￢parent(x,y)∨￢male(x)
に対して、各変数に HUs の全ての組み合わせを代入した
場合の各 HI({C3θ}) の値を求める。
代入θ={hiroshi/x, hiroshi/y} の場合:
parent(hiroshi, hiroshi) ∈HI より
HI({parent(hiroshi, hiroshi)}) =⊥。よって定義3.17 (p. 61)の
2より、 HI({￢(parent(hiroshi, hiroshi)}) = a
T。
よって、定義3.17の4 (p. 62)より、 HI({C3θ}) = b
T 。
代入θ ={hiroshi/x, maruko/y} の場合:
father(hiroshi, maruko) ∈HIより
HI ({father(hiroshi, maruko)}) = c
T 。よって、定義3.17の
4より、Val(C3θ)= d
T。
代入θ = θ3 ={maruko/x, hiroshi/y}と
θ = θ4 ={maruko/x, maruko/y}の場合:
male(maruko) ∈HI より HI({male(maruko)})= ⊥e。
よって定義3.17の2より、 HI({￢ male(maruko)}) = T
f 。
g。
よって定義定義3.17の4より、 HI({C3θ3})= HI({C3θ4})= T
以上より、全ての組み合わせに対してC3の値はTになる。
よって定義3.17の6より、 HI ({C3})= h
T。
以上より、エルブラン解釈HIは、節集合 S 中の全ての節
の値をTにするので、定義3.17の3より、 HI (S)= Ti 。
j
HI(S)= Tとなるエルブラン解釈はSのエルブランモデル
なので、 HIは Sのエルブランモデルである。
j
節集合 S を以下のようなものとする。
S={ parent(hiroshi,maruko),
male(hiroshi),
father(x,y)∨￢parent(x,y)∨￢male(x)}
答案の書き方
課題14-1 Sに対するエルブラン基底
HBs = { , … ,
}
10個全て書く
課題14-2 エルブラン解釈
HI = { parent(hiroshi,maruko), male(hiroshi),
father(hiroshi, maruko)}.
が、S のエルブランモデルであることの証明。
(a) …
(b) …
.
.
.
(j) …

Download Report