数理論理学　最終回 茨城大学工学部情報工学科 佐々木　稔.

Presentation on theme: "数理論理学　最終回 茨城大学工学部情報工学科 佐々木　稔."— Presentation transcript:

1 数理論理学　最終回 茨城大学工学部情報工学科 佐々木　稔

2 前回までのあらすじ http://sas.cis.ibaraki.ac.jp/logic/ 述語論理と導出原理 単一化置換
単一化アルゴリズム ファクタリング 配布資料は以下のURLからダウンロードできます

3 前回の問題 以下の文を考える。 「花子」は「松夫」の母親である。 「花子」は「太郎」の妻である。 「ｚ」は「ｙ」の父親である。 このとき、以下の導出節を単一化して、「誰」が「誰」の父親であるか答えなさい。 {母親(花子, 松夫), 妻(花子, 太郎), 　～母親(x, y)∨～妻(x,z)∨父親(z,y)}

4 前回の問題 {母親(花子, 松夫), 妻(花子, 太郎), ～母親(x, y)∨～妻(x,z)∨父親(z,y)}
母親(花子, 松夫)と母親(x, y)で単一化を行う。 不一致集合は{‘花子’=x, ‘松夫’=y} となるため、 x=‘花子’, y=‘松夫’ として単一化する。 妻(花子, 太郎)と妻(花子,z)で単一化を行う。 不一致集合は{‘太郎’=z} となるため、 z=‘太郎’ として単一化する。 その結果、父親(太郎, 松夫) となるので、 「太郎は松夫の父親である。」 となる。

5 今週のお題 述語論理と導出原理 エルブランの定理 導出原理 述語表現と推論

6 エルブランの定理 節集合 C の充足不能性を調べる 必要な知識 エルブラン領域 基礎列、エルブラン基底 エルブラン解釈

7 エルブラン領域 項が取り得る値の範囲 エルブラン領域 H の求め方 充足不能を調べる領域と等価なひとつの領域
i = 0, 1, 2, ・・・ について、 Hi+1 = Hi ∪{f(t1, t2, ・・・, tn)の集合} f は節集合に現れるすべての関数 t1, t2, ・・・, tn は Hi のすべての要素

8 エルブラン領域を求める例 C={P(x, a),Q(b, f(y))} のエルブラン領域 H0 = {a, b}
H1 = {a, b, f(a), f(b)} H2 = {a, b, f(a), f(b), f(f(a)), f(f(b))} 　　・・・ H = {a, b, f(a), f(b), f(f(a)), f(f(b)), f(f(f(a))), f(f(f(b))), ・・・}

9 基礎節 基礎節 エルブラン基底 HB(C) エルブラン解釈 節集合の各変数にエルブラン領域の要素を代入
P(a, a), Q(b, f(a)), P(b, a), Q(b, f(b)) エルブラン基底 HB(C) 基礎節のすべての集合 HB(C) = {P(a, a), Q(b, f(a)), P(b, a), Q(b, f(b)), P(f(a), a), Q(b, f(f(a))), ・・・} エルブラン解釈 エルブラン基底の各要素に真偽を割り当てたもの

10 エルブランの定理 エルブラン基底 エルブラン解釈 真となるエルブラン解釈がひとつでも存在
HB = {A1, A2, ・・・, Ai, ・・・} エルブラン解釈 HI1 = {　A1, 　A2, A3, ・・・} HI2 = {~A1, 　A2, A3, ・・・} HI3 = {　A1, ~A2, A3, ・・・} HI4 = {~A1, ~A2, A3, ・・・} 真となるエルブラン解釈がひとつでも存在 充足可能

11 エルブラン解釈 A1 ~A1 A2 ~A2 A2 ~A2 A3 ~A3 A3 ~A3 A3 ~A3 A3 ~A3 HI1 HI3 HI2

12 エルブランの定理 節集合 C が充足不能であるとき、そしてそのときに限り、意味木はすべての順路で偽となる節点に到達する

13 ひとつのエルブラン解釈の意味木 F F ~T∨F =F {~P(a)∨Q(f(a)), P(a), ~Q(f(a))} P(a) ~P(a)

14 導出原理 恒偽性を証明すべき節集合 C 中の2つの節 Ci, Cj を単一化 上の処理を繰り返す C = {C1, C2, ・・・, Cn}
導出節 Cij が空節ならば充足不能、 導出節 Cij が空節でなければ C に追加 上の処理を繰り返す 充足不能であれば空節が導出できる

15 導出原理の例 論理式 この論理式の節集合 この節集合から結論 ∃xC(x) を反駁定理で証明
∃x(A(x)∧∀y(A(y)⇒B(x)))∧(∀xB(x)⇒C(x)) この論理式の節集合 {A(a), ~A(y)∨B(a), ~B(x)∨C(x)} この節集合から結論 ∃xC(x) を反駁定理で証明

16 導出原理の例 結論 ∃xC(x) の否定 空節を求めるべき節集合は以下になる 単一化を行いながら導出木により空節を導く
~∃xC(x) = ∀x~C(x) 空節を求めるべき節集合は以下になる {A(a), ~A(y)∨B(a), ~B(x)∨C(x), ~C(x)} 単一化を行いながら導出木により空節を導く

17 反駁導出による証明 □ A(a) ~A(y)∨B(a) B(a) ~B(x)∨C(x) C(a) ~C(x) [ y = a ]
[ x = a ] C(a) ~C(x) [ x = a ] □ 矛盾するため、 ∃xC(x) は成り立つ （証明終わり）

18 述語表現と推論 ペアノの公理（自然数についての規則） 次の式を満たす集合 N 1∈N x∈N ならば、σ(x)∈N
x≠y ならば、σ(x)≠σ(y) x∈N ならば、σ(x)≠1 N の部分集合 S が以下を満たすとき、 S=N 1∈S x∈S ならば、σ(x)∈S

19 ペアノの公理 述語により記述 N(x) : x は自然数である S(x) : x は集合 S の要素である
EQ(x, y) : x と y は同じである s(x) : σ(x)

20 ペアノの公理（述語論理版） N(1) ∀xN(x) ⇒ N(s(x)) ∀x∀y(~EQ(x, y) ⇒ ~EQ(s(x), s(y)))
∀x(N(x) ⇒ ~EQ(s(x), 1)) ∀x(S(x)⇒N(x))∧(S(1)∧∀x(S(x) ⇒S(s(x)))⇒∀y(S(y)⇔N(y)))

21 自然数の加算 次の数を表す関数 s(x) 加算(x+y=z)を表す述語 Plus(x, y, z)
s(0)=1, s(s(0))=2, s(s(s(0)))=3, ・・・ s(s(・・・s(0))) = n 加算(x+y=z)を表す述語 Plus(x, y, z) Plus(x, y, z) を関数 s を用いて定義 n 個

22 自然数の加算 以下の式を仮定 2+3を計算 0+x=x x+y=z ⇒ (x+1)+y=(z+1) 結論 Plus(0, x, x)
Plus(x, y, z) ⇒ Plus(s(x), y, s(z)) 2+3を計算 結論 ∃xPlus(s(s(0)), s(s(s(0))), x)

23 加算の定義と結論から得られる節集合 {Plus(0, x, x), 　　　　　　　　　　　　　　　　　～Plus(x, y, z)∨Plus(s(x), y, s(z)), ～Plus(s(s(0)), s(s(s(0))), x) }

24 ～Plus(x1, y1, z1) ∨ Plus(s(x1), y1, s(z1)) ～Plus(s(s(0)), s(s(s(0))), x) [x1 = s(0), y1 = s(s(s(0))), x = s(z1) ] ～Plus(x2, y2, z2) ∨ Plus(s(x2), y2, s(z2)) ～Plus(s(0), s(s(s(0))), z1) [x2 = 0, y2 = s(s(s(0))), z1 = s(z2) ] ～Plus(0, s(s(s(0))), z2)

25 導出の続き (空節) ～Plus(0, s(s(s(0))), z2) Plus(0, x3, x3) [x3 = s(s(s(0))),
z2 = s(s(s(0))) ] (空節)

26 x には何が代入されているの？ x = s(z1) z1 = s(z2) z2 = s(s(s(0))) よって、
x= s(z1) = s(s(z2)) = s(s(s(s(s(0)))))

27 練習問題 節集合{～F(x)∨G(x), ～G(a)}から、∃x～F(x)を証明せよ。
論理式 Plus(0, x, x)、 Plus(x, y, z) ⇒ Plus(s(x), y, s(z)) から、1+1の計算を行う論理式 ∃xPlus(s(0), s(0), x) を証明し、xに入る値を求めよ。 節集合{～F(x)∨G(x), ～G(a)}から、∃x～F(x)を証明せよ。