数理論理学第2 回 - Sasaki Laboratory | Just

数理論理学第12回
茨城大学工学部情報工学科
佐々木稔
前回までのあらすじ
 スコーレム標準形
 配布資料は以下のURLからダウンロードできます
http://sas.cis.ibaraki.ac.jp/logic/
今週のお題
 導出と推論
 導出とは
 反駁導出
 述語論理と導出原理
 単一化置換
 単一化アルゴリズム
 ファクタリング
導出とは
 肯定式
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
導出
 推論規則の法則
 ある述語の正のリテラルを含む選言式
 その述語の負のリテラルを含む選言式
 以上の2つの選言式から
 その述語を削除した選言式を導くことができる
p∨Q
~p ∨ R
Q∨R
導出節
反駁導出
 論理式 P
 P = P1∧P2∧・・・∧Pm
 論理式 P から、ある論理式 Q が導ける
 P1∧P2∧・・・∧Pm ⇒ Q
 背理法より、下の論理式が恒偽なのと同値
 P1∧P2∧・・・∧Pm∧~Q
 次の節形式が矛盾することでQの証明が可能
 {P1, P2, ・・・, Pm , ~Q}
反駁導出による証明方法
 節形式から以下の２つの節を取り出す
 { ･･･, p ∨ Q, ~p ∨ R, ･･･}
 導出した新しい節を節形式に加える
 { ･･･, Q ∨ R, ･･･}
 2つの節が同一述語で正負のリテラルの場合、
 { ･･･, p, ~p, ･･･}
 導出により、何も残らない（空節）
 { ･･･, □, ･･･}
反駁導出による証明方法
 反駁木
 導出過程を木構造で表現
 節集合 {A(a), ~A(y)∨B(a), ~B(x)∨C(x)}
 ∃xC(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) は成り立つ（証明終わり）
単一化置換
 一般的に述語の引数は変数
 2つの節に共通な正負のリテラルにならない
 単一化
 2つのリテラルが~記号を除いて一致させる
 変数に適当な基礎項（または項）を割り当てる
 単一化置換
 各変数への割り当て方法
単一化置換
 置換 σ
 変数 vi を適当な項 ti (i=1, 2, ・・・, n)で置換
 σ= [v1=t1, v2=t2, ・・・, vn=tn]
単一化置換の例
 P(x, y, f(x)) と P(a, g(z), w) を単一化
 単一化例
 [x=a, y=g(z), w=f(a)]
 y=g(z) に変数 z が残る
 後で必要なときに基礎項に置き換えてよい
 最汎単一化置換（最大単一化置換）
単一化置換
 不一致集合
 リテラル間の不一致部分の抽出した集合
 一致する置換をすべての項で求める
 最汎単一化が可能
不一致集合の例
 P(a, f(g(x)), x) と P(a, f(y), g(z))
 文字列 “P(a, f(” まで同じ文字列
 その次の文字を含む項が不一致集合
 [g(x)=y]
 次の不一致部分
 [x=g(z)]
 よって、最汎単一化置換は
 [g(g(z))=y, x=g(z)]
単一化アルゴリズム


1.
2.
L={P1, P2} を単一化する置換σを求める
アルゴリズム
同じ記号の変数を区別するように付け替える
L の不一致集合 D を求めて、
1. D が空集合の場合、それまでのσが最汎単一化
2. D に変数 vi と項 ti があり、置換可能ならば、
vi = ti をσに追加
3. 一致可能な置換がなければ、単一化できない
3. L に置換を行って、2. に戻る
単一化の例
 L={P(x, f(x), y), P(a, y, g(x))}
 変数名の付け替え
 L={P(x1, f(x1), y1), P(a, y2, g(x2))}
 不一致集合 D を求める
 D = {x1, a}
 x1=a をσに追加
 σ = [ x1=a ]
 L を置換
 L={P(a, f(a), y1), P(a, y2, g(x2))}
単一化の例
 L={P(a, f(a), y1), P(a, y2, g(x2))}
 不一致集合 D を求める
 D = {f(a), y2}
 y2=f(a) をσに追加
 σ = [ x1=a, y2=f(a) ]
 L を置換
 L={P(a, f(a), y1), P(a, f(a), g(x2))}
単一化の例
 L={P(a, f(a), y1), P(a, f(a), g(x2))}
 不一致集合 D を求める
 D = {y1, g(x2)}
 y1=g(x2) をσに追加
 σ = [ x1=a, y2=f(a), y1=g(x2) ]
 L を置換
 L={P(a, f(a), g(x2)), P(a, f(a), g(x2))}
 単一化終了
ファクタリング
 ひとつの節に同じ述語が存在
 {S(x)∨S(y), ~S(u)∨~S(v)}
 まとめることが可能（ファクタリング）
 [ x = y, u = v ] でファクタリング
 {S(x) ~S(u)}
 ファクタリングはあらかじめ行う
 空節が導出できない場合がある

Download Report