数理論理学　第12回 茨城大学工学部情報工学科 佐々木　稔

前回までのあらすじ http://sas.cis.ibaraki.ac.jp/logic/ スコーレム標準形 配布資料は以下のURLからダウンロードできます http://sas.cis.ibaraki.ac.jp/logic/

前回の問題 次の述語論理式をスコーレム標準形に変換せよ。 ∀x∃y(P(x, y)⇒Q(x)) =∀x∃y(~P(x, y)∨Q(x)) y = f(x) と置くと、 =∀x(~P(x, f(x))∨Q(x))

前回の問題 次の述語論理式をスコーレム標準形に変換せよ。 ~(∀x∃y((P(x, y)⇒~R(y))∧∀zR(z))) = ~∀x∃y((~P(x, y)∨~R(y))∧∀zR(z)) = ∃x∀y(~(~P(x, y)∨~R(y))∨~∀zR(z)) = ∃x∀y((P(x, y)∧R(y))∨∃z~R(z)) x = a, z=g(y) と置くと、 = ∀y((P(a, y)∧R(y))∨~R(g(y))) = ∀y((P(a, y)∨~R(g(y)))∧(R(y)∨~R(g(y))))

今週のお題 スコーレム標準形（復習） 導出と推論 導出とは 反駁導出 述語論理と導出原理 単一化置換 単一化アルゴリズム ファクタリング

スコーレム標準形 量記号のスコープ内に束縛変数がなければ、量記号を削除 ⇒、⇔記号を~、∨、∧記号で書き換える ~記号を基本論理式の直前に移動 束縛変数の付け替え スコーレム関数を導入し、存在記号を除去 全称記号を左に移す 分配律などで、連言に統一

変換例１ ∀x∃y(P(x, y)⇒Q(x)) ∀x∃y(～P(x, y)∨Q(x)) ∀x(～P(x, f(x))∨Q(x)) ⇒記号の除去 ∀x∃y(～P(x, y)∨Q(x)) スコーレム関数を導入し、存在記号を除去 ∀x(～P(x, f(x))∨Q(x))

変換例２ ～(∀x∃y((P(x, y)⇒R(y))∧∀zR(z))) ～(∀x∃y((～P(x, y)∨R(y))∧∀zR(z))) ⇒記号の除去 ～(∀x∃y((～P(x, y)∨R(y))∧∀zR(z))) ~記号を基本論理式の直前に移動 ∃x∀y(～(～P(x, y)∨R(y))∨～∀zR(z)) ∃x∀y((P(x, y)∧～R(y))∨∃z～R(z))

変換例２（続き） ∃x∀y((P(x, y)∧～R(y))∨∃z～R(z)) ∀y((P(a, y)∧～R(y))∨～R(f(y))) スコーレム関数を導入し、存在記号を除去 ∀y((P(a, y)∧～R(y))∨～R(f(y))) 分配律 ∀y( ( P(a, y)∨～R(f(y)) ) ∧( ～R(y)∨～R(f(y)) ) )

変換例3 ∀x∃y(P(x, y)⇒Q(x)) ∧～(∀x∃y((P(x, y)⇒R(y))∧∀zR(z))) ∀x(～P(x, f(x))∨Q(x)) ∧ ∀y((P(a, y)∨～R(f(y)))∧(～R(y)∨～R(f(y))))

練習１（教科書168ページの問題19） ~∃x∃y(~p(x)∧∀z q(y, z))

練習１の解答例 ~∃x∃y(~p(x)∧∀z q(y, z)) ~記号を基本論理式の直前に移動 z = f(x, y) とおいて、 ∀x∀y(p(x)∨~q(y, f(x, y)))

導出とは 肯定式 もしくは、 P ⇒ Q P Q ~P ∨ Q P Q

導出 否定式１ もしくは、 P ⇒ Q ~Q ~P ~P ∨ Q ~Q ~P

導出 否定式２ P ∨ Q ~P Q

導出 否定式３ もしくは、 P 　 Q P ~Q （P ∨ Q）∧（~P ∨ ~Q） P ~Q

導出 三段論法 もしくは、 P ⇒ Q Q ⇒ R P ⇒ R ~P ∨ Q ~Q ∨ R ~P ∨ R

導出 三段論法 もしくは、 P ⇒ Q R ⇒ ~Q P ⇒ ~R ~P ∨ Q ~R ∨ ~Q ~P ∨ ~R

導出 導出節 p ∨ Q ~p ∨ R Q ∨ R 推論規則の法則 ある述語の正のリテラルを含む選言式 その述語の負のリテラルを含む選言式 以上の2つの選言式から その述語を削除した選言式を導くことができる 　p ∨ Q ~p ∨ R 　Q ∨ R 導出節

反駁導出 論理式 P 論理式 P から、ある論理式 Q が導ける 背理法より、下の論理式が恒偽なのと同値 P = P1∧P2∧・・・∧Pm 論理式 P から、ある論理式 Q が導ける P1∧P2∧・・・∧Pm ⇒ Q 背理法より、下の論理式が恒偽なのと同値 P1∧P2∧・・・∧Pm∧~Q 次の節形式が矛盾することでQの証明が可能 {P1, P2, ・・・, Pm , ~Q}

反駁導出による証明方法 節形式から以下の２つの節を取り出す 導出した新しい節を節形式に加える 2つの節が同一述語で正負のリテラルの場合、 { ･･･, p ∨ Q, ~p ∨ R, ･･･} 導出した新しい節を節形式に加える { ･･･, Q ∨ R, ･･･} 2つの節が同一述語で正負のリテラルの場合、 { ･･･, p, ~p, ･･･} 導出により、何も残らない（空節） {}

反駁導出による証明方法 反駁木 導出過程を木構造で表現 節集合 {A(a), ~A(y)∨B(a), ~B(x)∨C(x)} 便宜上、x, y はすべて a と置き換える 以下の節集合を反駁導出により証明 {A(a), ~A(a)∨B(a), ~B(a)∨C(a), ~C(a)}

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

練習問題 次の述語論理式をスコーレム標準形に変換せよ。 ∀x∃y(P(x, y)⇒Q(x))⇒∀x∀y(R(x, y)⇒S(x))