●命題論理の演繹体系 ○導出原理 リテラル(literal) 原子論理式かその否定 節(clause) リテラルを∨で結んだもの。 L1∨L2∨...∨Ln n=0の場合、空節という。 空節を⊥と書く。 節におけるリテラルの順序および重複は無視する。 すなわち、節はリテラルの有限集合と考えられる。 CやDは節を表すとする。 連言標準形 節の連言を、連言標準形(conjunctive normal form)という quantifierを含まない任意の論理式に対して、 それと等価な連言標準形に変換することができる。 連言標準形は、節の有限集合と考えることができる。 導出原理(resolution principle) 節A∨Cと節¬A∨Dから節C∨Dを導く。 A: 原子論理式 C,D: 節(の残り) 分解ともいう。 Δ: 閉じた節の有限集合 すなわち、変数を含まない連言標準形。 反駁(refutation) ⊥が得られるまで導出を繰り返す。 while not(⊥∈Δ) do choose A∨C and ¬A∨D in Δ Δ := Δ∪{C∨D} 反駁の完全性 Δから⊥が導出可能 iff Δ: 充足不能 →は明らか。(すなわち、導出原理は健全である。) Δが充足不能ならばΔから⊥が導出可能なことを示す。 Δに含まれる原子論理式の数に関する帰納法 原子論理式が一つもなければ、⊥しか有り得ない。 AをΔに現れる原子論理式とする。 Aを真と仮定しても充足不能である。 従って、ΔからAを含む節を除き、 残った節から¬Aを除いた結果Δ'も充足不能である。 帰納法の仮定より、Δ'から⊥が導出可能である。 Δ'からの⊥の導出に¬Aを戻す。 すると、Δから⊥もしくは¬Aが導出可能である。 Aを偽と仮定しても充足不能である。 従って、Δから¬Aを含む節を除き、 残った節からAを除いた結果Δ"も充足不能である。 帰納法の仮定より、Δ"から⊥が導出可能である。 Δ"からの⊥の導出にAを戻す。 すると、Δから⊥もしくはAが導出可能である。 ΔからAと¬Aが導出可能ならば、 Δから⊥が導出可能である。 ○ホーン節と単位導出および入力導出 正リテラル 原子論理式 負リテラル 原子論理式の否定 単位節(unit clause) 一つのリテラルから成る節 正単位節(unit clause) 一つの正リテラルから成る節 負単位節(unit clause) 一つの負リテラルから成る節 ホーン節(Horn clause) 正リテラルを高々一つ含む節 確定節(definite clause) 正リテラルをちょうど一つ含む節 負節(negative clause) 正リテラルを一つも含まない節 単位導出(unit resolution) 片方の前提が単位節である導出 正単位導出 片方の前提が正単位節である導出 Δ: 閉じたホーン節の有限集合 Δが充足不能ならば、 Δから正単位導出のみを用いて⊥が導出可能である。 入力節(input clause) もとのΔに含まれる節 入力導出(input resolution) 片方の前提が入力節である導出 Δ: 閉じたホーン節の有限集合 Δが充足不能ならば、 Δから入力導出のみを用いて⊥が導出可能である。 ○その他の演繹体系 シーケント計算 自然演繹 ヒルベルト流 ●述語論理の演繹体系 ○代入 代入とは、変数から項への関数(写像)のことである。 ただし、有限個の変数を除いて、変数をそれ自身に写す。 従って、代入は、 [x1:=t1, ..., xn:=tn] と書くことができる。 xiを同時にtiに置き換える。 代入は項へ適用することができる。 θ(xi) = ti θ(x) = x if x is not in {x1,...,xn} θ(f(t1,...,tn)) = f(θ(t1),...,θ(tn)) tθというように、代入を項の後ろに書くこともある。 代入の合成 代入θ1とθ2が与えられたとき、任意の項tに対して、 θ1(θ2(t)) = ψ(t) を満たす代入ψが存在する。この代入ψをθ1θ2と書く。 実際に、θ1が[x1:=t1,...,xn:=tn]、 θ2が[y1:=u1,...,ym:=um]であるとき、ψは、 [y1:=θ1(u1),...,ym:=θ1(um),x1:=t1,...,xk:=tk] となる。ただし、x1,...,xnのうち、 y1,...,ymに現れないものをx1,...,xkとした。 unifier 項t1,...,tnに対して、 θ(t1) = ... = θ(tn) となる代入θを、t1,...,tnのuniferという。 unifierが存在するとき、t1,...,tnはunify可能であるという。 mgu 項t1,...,tnのmgu(most general unifier)とは、 t1,...,tnのunifierθであって、 t1,...,tnの任意のunifierψに対して、 ψ = ξθ となるξが存在するもののこと。 例えば、f(x,x)とf(y,c)のmguは、 [x:=c, y:=c] mguはuniqueではない。 例えば、f(x,x)とf(y,z)のmguは、 [x:=z, y:=z] [x:=y, z:=y] [y:=x, z:=x] ただし、mgu同士は、変数の名前を替えることで移り合える。 t1,...,tnがunify可能ならば、 t1,...,tnのmguが存在する(計算することができる)。 t1とt2のmguの計算 t1が変数xであるとき。 t2も変数xならば空の代入[]を返す。 xがt2に現れるかどうかを検査する(occur check)。 xがt2に現れれば、t1とt2はunify不可能。 xがt2に現れなければ、 代入[x:=t2]を返す。 t2が変数xであるとき。上と同様。 t1とt2が、 f(t11,...,t1m)とf(t21,...,t2m) という形をしているとき。 t11とt21のmguθ1を求める。 θ1(t12)とθ1(t22)のmguθ2を求める。 θ2(θ1(t13))とθ2(θ1(t23))のmguθ3を求める。 ... θm-1(...(θ1(t1m))),...,θm-1(...(θ1(t2m)))のmguθmを求める。 θm...θ1を返す。 (m=0ならば空の代入[]が返る。) その他の場合は、t1とt2はunify不可能。 t1,...,tnのmguの計算 t1とt2のmguθ1を求める。 θ1(t2)とθ1(t3)のmguθ2を求める。 θ2(θ1(t3))とθ2(θ1(t4))のmguθ3を求める。 ... θn-2(...(θ1(tn-1)))とθn-2(...(θ1(tn)))のmguθn-1を求める。 θn-1...θ1を返す。 ○導出原理 Δ: 節の集合 変数を含むかもしれない。 導出原理 A1,...,Amを、同じ述語記号で始まる原子論理式とする。 以下の形の二つの節を選ぶ。 A1∨...∨An∨C ¬An+1∨...∨¬Am∨D ただし、二つの節の間で同じ変数が現れないように、 あらかじめ変数の名前を適当に換えておく。 A1,...,Amのmguをθとする。このとき、 上の二つの節から、 Cθ∨Dθ を得ることを導出という。 lifting Δ': Δの節の閉じた具体例(instance)の集合 節Cの具体例とは、ここでは、ある代入θがあって、 θ(C)と書ける節のこと。 節はリテラルの有限集合であるから、節Cに代入θを施すと、 Cでは異なっていたリテラルが潰れて一つになることも有り得る。 Δ'から導出される任意の節C'に対して、 Δから導出される節Cが存在して、C'はCの具体例となる。 導出のステップ数に関する帰納法。Δ'から導出可能な二つの節 A'∨C' ¬A'∨D' を、それぞれ、Δから導出可能な二つの節 A1∨...∨An∨C ¬An+1∨...∨¬Am∨D の具体例とする。すなわち、代入θ1とθ2に対して、 A'∨C' = θ1(A1∨...∨An∨C) A' = θ1(Ai) C' = θ1(C) ¬A'∨D' = θ2(¬An+1∨...∨¬Am∨D) A' = θ2(Ai) D' = θ2(D) とする。A1∨...∨An∨Cと¬An+1∨...∨¬Am∨Dは、 変数を共有しないように変数の名前を換えておくので、 A'∨C' = θ1θ2(A1∨...∨An∨C) ¬A'∨D' = θ1θ2(¬An+1∨...∨¬Am∨D) としてよい。従って、A1,...,Amはunify可能である。 すると、A1,...,Amのmguθが存在するので、 θ(C∨D) はΔから導出可能である。θはmguなので、あるξが存在して、 θ1θ2 = ξθ が成り立つ。従って、 C'∨D' = θ1θ2(C∨D) = ξθ(C∨D) = ξ(θ(C∨D)) となる。すなわち、C'∨D'はθ(C∨D)の具体例である。 ○paramodulation(参考) --- 導出原理における等号推論 L[t]は項tを含むリテラル。 paramodulationとは、 C∨t=u L[t]∨D から C∨L[u]∨D を導くこと。 L[u]は、L[t]の中のtの出現の一つを、 uで置き換えたもの。 また、 ¬t=t∨C から C を導く操作も許す。 変数がある場合は、 C∨t=u L[t']∨D から θ(C∨L[u]∨D) を導く。θはtとt'のmgu。 また、 ¬t=t'∨C から θ(C) を導く。θはtとt'のmgu。 ○その他の演繹体系 ヒルベルト流 自然演繹 シーケント計算 ○ヒルベルト流 ここでは、命題論理の部分は、 任意のトートロジーおよびトートロジーの命題記号を 論理式で置き換えたもの(tautological instance)を 公理として認めてしまう。 Modus Ponens: AとA⊃BからBを導出。 従って、A⊃Bがトートロジーの場合、 AからBを導くことができる。 ∀に関する公理: ∀x A[x]⊃A[t] 代入の公理 ∀x(A⊃B[x])⊃(A⊃∀x B[x]) ただし、Aにxは自由に現れない。 この逆は、代入と汎化により得られる。 汎化: A[x]から∀x A[x]が導かれる。 ∃x A[x]は¬∀x(¬A[x])の略とする。 A[t]⊃∃x A[x] 代入の公理 派生規則として以下のようなものが得られる。(汎化の一種) A⊃B[x]からA⊃∀x B[x]が得られる。 ただし、Aにxは自由に現れない。 A[x]⊃Bから∃x A[x]⊃Bが得られる。 ただし、Bにxは自由に現れない。 公理から導出される論理式を定理という。 ○シーケント計算 演習 ●一階述語論理の完全性 定理は恒真である。(健全性) 恒真の論理式は定理である。(完全性) A: 恒真 ∀x1...∀xn A: 恒真 ¬∀x1...∀xn A: 充足不能 これと同値な冠頭標準形を求める。 同値性を定理として証明する必要はある。 例えば、 ∀x∃y∀v∃w A[x,y,v,w] とする。Skolem化: ∀x∀v A[x,f(x),v,g(x,v)] Herbrandの定理より、例えば、 A[t1,f(t1),s1,g(t1,s1)]∧ A[t2,f(t2),s2,g(t2,s2)]∧ A[t2,f(t2),s3,g(t2,s3)]⊃⊥ (*) がトートロジーである。これから、 ∀x∃y∀v∃w A[x,y,v,w] ⊃ ⊥ が導かれる。 ヒルベルト流の場合: A[t1,f(t1),s1,g(t1,s1)]∧ A[t2,f(t2),s2,g(t2,s2)]∧ A[t2,f(t2),s3,g(t2,s3)]⊃⊥ の証明(命題論理における証明)の中の f(t1) を y1 で f(t2) を y2 で g(t1,s1) を w1 で g(t2,s2) を w2 で g(t2,s3) を w3 で 置き換える。すなわち、Skolem関数で始まる項を、 それぞれにユニークに対応する新しい変数で置き換える。 すると、 A[t1,y1,s1,w1]∧A[t2,y2,s2,w2]∧A[t2,y2,s3,w3]⊃⊥ (**) はトートロジーである。従って証明可能である。 正確には、t1,t2,s1,s2,s3 の中に、 Skolem関数で始まる項が現れている場合は、 これらの項においても、上記の置き換えが行われる。 ただし、A[_,_,_,_]の部分にはSkolem関数は現れないので、 変化は受けない。 結果として、Skolem関数が現れない論理式(**)が得られる。 論理式(*)において同一の原子論理式は、 論理式(**)においても同一になる。 したがって、(**)もトートロジーである。 (*)に対して汎化を繰り返して、 ∃w A[t1,y1,s1,w]∧ ∃w A[t2,y2,s2,w]∧ ∃w A[t2,y2,s3,w]⊃⊥ が得られる。代入の公理より、 ∀v∃w A[t1,y1,v,w]∧ ∀v∃w A[t2,y2,v,w]⊃⊥ が求まる。再び汎化を繰り返す。 ∃y∀v∃w A[t1,y,v,w]∧ ∃y∀v∃w A[t2,y,v,w]⊃⊥ 最後に、代入の公理より、 ∀x∃y∀v∃w A[x,y,v,w]⊃⊥ が得られる。 ただし、汎化と代入の順序は、 t1,t2,s1,s2,s3 に y1,y2,w1,w2,w3 が現れるかどうかに従って、 適当に入れ換える必要がある。 例えば、t2 に w1 が現れる場合 (すなわち、もともとの t2 に s1 が現れる場合)、 w1 に関する汎化を先に行うことができないので、 w2,w3,y2 に関する汎化と関連する代入を先に行う。 A[t1,y1,s1,w1]∧ ∀x∃y∀v∃w A[x,y,v,w]⊃⊥ t2 が消えたので、w1 に関する汎化を行うことができる。 ∃w A[t1,y1,s1,w]∧ ∀x∃y∀v∃w A[x,y,v,w]⊃⊥ 結局、t1,t2,s1,s2,s3 の間の包含関係に従った順序で汎化を行う。 すなわち、大きい方の項を置き換えた変数の汎化を先に行う。 シーケント計算の場合: 同様に、 A[t1,f(t1),s1,g(t1,s1)],A[t2,f(t2),s2,g(t2,s2)],A[t2,f(t2),s3,g(t2,s3)]→⊥ の証明(命題論理における証明)の中の f(t1) を y1 で f(t2) を y2 で g(t1,s1) を w1 で g(t2,s2) を w2 で g(t2,s3) を w3 で 置き換える。すると、 A[t1,y1,s1,w1],A[t2,y2,s2,w2],A[t2,y2,s3,w3]→⊥ の証明が得られる。従って、 A[t1,y1,s1,w1],A[t2,y2,s2,w2],A[t2,y2,s3,w3]→⊥ ------------------------------------------------ ∃w A[t1,y1,s1,w],∃w A[t2,y2,s2,w],∃w A[t2,y2,s3,w]→⊥ --------------------------------------------------------------- ∀v∃w A[t1,y1,v,w],∀v∃w A[t2,y2,v,w],∀v∃w A[t2,y2,v,w]→⊥ --------------------------------------------------------------- ∀v∃w A[t1,y1,v,w],∀v∃w A[t2,y2,v,w]→⊥ ----------------------------------------------- ∃y∀v∃w A[t1,y,v,w],∃y∀v∃w A[t2,y,v,w]→⊥ --------------------------------------------------- ∀x∃y∀v∃w A[x,y,v,w],∀x∃y∀v∃w A[x,y,v,w]→⊥ --------------------------------------------------- ∀x∃y∀v∃w A[x,y,v,w]→⊥