数理論理学第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)}  ファクタリングはあらかじめ行う  空節が導出できない場合がある