数理論理学

第14回

​

導出原理の健全性と完全性

エルブランの定理

© 加藤，高田，新出

4.3節(p. 104)

導出原理の健全

性と完全性

課題13 節集合S に対する導出原理を行え

節 (2) と (3)を用いて導出を行う。このときのmgu は{w/y, sakiko/x}.

child(sakiko, w) ∨￢parent(w,sakiko)

　 ￢ child(sakiko,w)

S={ parent(hiroshi, sakiko), 　　　　　 (1)

child(x, y) ∨￢parent(y,x), 　(2)

￢ child(sakiko,w) (3)

}

　　　　　　　　　　 (a)

このmgu を節(2)と(3)に適用すると、以下のようになる。

(c)

　　　　　　　　　 　　　(b)

導出の結果、次の　　導出節　　が残る。

￢parent(w, sakiko).

これと、節 (1) から導出を行う。 mgu は{hiroshi/w}.

￢parent(hiroshi , sakiko)

parent(hiroshi , sakiko)

​

□ 導出の結果、空節 が求まる。

　　　　　　　(d)

　　　　　　 (e)

節(1)を使って導出を進める。

　　　　　　　　　 (f)

(g)

(h)

導出原理の健全性　(p. 104)

節集合 S から導出原理によって空節を

得れば， S は充足不能 である。

{ parent(hiroshi, maruko)

child(x, y) ∨￢parent(y, x)

￢ child(maruko, w) }

(p. 65)

論理式や、関数に意味を

与えるもの。　(p. 61)

解釈

3.2.2 解釈

定義 3.17

割り当て

割り当て

さくら家における解釈を

とする。ただし

さくら家における解釈を

とする。ただし

導出原理の健全性　 (p. 104)

節集合 S から導出原理によって空節を

得れば， S は充足不能 である

(p. 65)

どんな解釈を持ってきても、S のモデルにはならない

{ parent(hiroshi, maruko)

child(x, y) ∨￢parent(y, x)

￢ child(maruko, w) }

導出原理の完全性 (p. 104)

充足不能な節集合 S に対して導出原理

により必ず空節を得る

{ parent(hiroshi, maruko)

child(x, y) ∨￢parent(y, x)

￢ child(maruko, w) } S1

S2

S3

S4

Sn

どんな解釈を持ってきても、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)

エルブランの定理 (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)

定義4.16 エルブラン領域HUS (p. 105)

HU0=

Constants(S) (Constants(S) ≠ ∅)

{a} (Constants(S) = ∅)

HU0={sumire,maruko}

= HUS

(S に関数記号が

　ないので (p. 106 l.4) )

(空集合)

定義4.16 エルブラン領域HUS (p. 105)

HU0=

Constants(S) (Constants(S) ≠ ∅)

{a} (Constants(S) = ∅)

HUi+1= HUi ∪{f(t1,…,tn) | ・・・・・・・・・}

HUS =∪HUi

i ∈ω

S 内に関数記号がある場合

{ sum(0, x, x),　　　　　　　　

￢sum(x, y, z)∨sum(succ(x), y, succ(z))}

HU0 = {0}

HU1 = {0, succ(0)}

HU2 = {0, succ(0), succ(s(0))}

HU3 = {0, succ(0), succ(succ(0)), …}

S

定義4.16 エルブラン領域HUS (p. 105)

例4.20 (pp. 106-107)

定義4.16 エルブラン領域HUS (p. 105)

HU0=

Constants(S) (Constants(S) ≠ ∅)

{a} (Constants(S) = ∅)

HU0={sumire,maruko}

= HUS

(S に関数記号が

　ないので (p. 106 l.4) )

(空集合)

エルブランの定理 (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)

定義4.17 エルブラン基底 (p. 105)

HBS = {p(t1,…,tm) | p は S に現れるarity m

の述語記号, t1,…,tm ∈ HUS }　

HUS={sumire,maruko}

HBS={female(sumire), female(maruko), …

定義4.17 エルブラン基底 (p. 105)

HUS={sumire,maruko}

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

定義4.17 エルブラン基底

HUs

{ sum(0, x, x),　　　　　　　　

￢ sum(x, y, z) ∨ sum(succ(x), y, succ(z))}

例4.20 (pp. 106-107)

2

3

S

エルブランの定理 (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)

定義4.18 割り当てAS　 (p. 105)

​

　　 以前の割り当て

定義3.15 (pp. 56-59)

​

定義4.18 割り当てAS　 (p. 105)

AS は HBS　の部分集合 (AS　⊆　HBS)(定義のl.2)

AS

={parent(sumire, maruko), (p. 106 ll. 7)

female(sumire), mother(sumire,maruko)}

AS

={parent(sumire, maruko),

female(sumire), mother(sumire,maruko)}

AS（parent(sumire, maruko)) = T (p. 106 ll. 6)

AS（female(sumire)) = T (p. 106 ll. 6)

AS（mother(sumire,maruko)) = T (p. 106 ll. 5)

AS（parent(maruko, maruko)) =⊥

エルブランの定理 (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)

以前の解釈 (pp. 61-65)

解釈

3.2.2 解釈

定義 3.17

定義4.18 割り当てAS　 (p. 105)

​

　　 以前の領域と割り当て

定義3.15 (pp. 56-59)

​

エルブラン領域

割り当て

定義4.19 エルブラン解釈と

　　　　　　　　　　　　エルブランモデル (p. 107)

HBS = {bird(hawk), bird(eagle),

fly(hawk), fly(eagle)}

HUs = {hawk, eagle}

エルブラン解釈

HUs = {hawk, eagle}

AS =HBS = {bird(hawk), bird(eagle),

fly(hawk), fly(eagle)}

C1

C2

C3

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

HUs = {hawk, eagle}

AS =HBS = {bird(hawk), bird(eagle),

fly(hawk), fly(eagle)}

C1

C2

C3

・ HI({fly(x) θ∨ ￢ bird(x) θ })=T ? (l. 8)

・ θ ={hawk/x}のとき

　　　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が充足不能

​

Sの基礎節集合GCS のある有限集合が

充足不能である。

iff

定義 4.20 基礎節集合　GCS (p. 109)　

HUs = {hawk, eagle}

GCS ={ bird(hawk),　

bird(eagle),　　　　　

fly(hawk) ∨ ￢ bird(hawk),

fly(eagle) ∨ ￢ bird(eagle) }

課題14-1 S に対するエルブラン基底

(要素10個)を求めよ。　

S=

{parent(hiroshi,maruko), C1

male(hiroshi), C2

father(x,y)∨￢parent(x,y)∨￢male(x) C3}

}　を節集合とする。

課題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}

解答

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)

}

HUs = {hiroshi, maruko}

Sの一つのエルブラン解釈 HI を以下のように取るとき、

この 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)}) = T 。

よって、定義3.17の4 (p. 62)より、 HI({C3θ}) = T 。

a

b

HI = {parent(hiroshi,maruko), male(hiroshi), father(hiroshi, maruko)}.

代入θ ={hiroshi/x, maruko/y} の場合:　

father(hiroshi, maruko) ∈HIより

HI ({father(hiroshi, maruko)}) =　 T 。よって、定義3.17の

4より、Val(C3θ)= T 。

代入θ = θ3 ={maruko/x, hiroshi/y}と

θ = θ4 ={maruko/x, maruko/y}の場合:

male(maruko) ∈HI より HI({male(maruko)})= ⊥ 。

よって定義3.17の2より、 HI({￢ male(maruko)}) = T 。

よって定義定義3.17の4より、 HI({C3θ3})= HI({C3θ4})= T 。

以上より、全ての組み合わせに対してC3の値はTになる。

よって定義3.17の6より、 HI ({C3})= T 。

以上より、エルブラン解釈HIは、節集合 S 中の全ての節

の値をTにするので、定義3.17の3より、 HI (S)= T 。

HI(S)= Tとなるエルブラン解釈はSのエルブランモデル

なので、 HIは Sのエルブランモデルである。

c

d

e

f

g

h

i

j

j

1. …
2. …

.

.

.

(j) …

HBs = { , … , }

答案の書き方

節集合 S を以下のようなものとする。

S={ parent(hiroshi,maruko),

male(hiroshi),

father(x,y)∨￢parent(x,y)∨￢male(x)}　

課題14-1 Sに対するエルブラン基底

10個全て書く

課題14-2 エルブラン解釈

HI = { parent(hiroshi,maruko), male(hiroshi),

father(hiroshi, maruko)}.

が、S のエルブランモデルであることの証明。

​