導出原理
反駁(はんばく、英: refutation)とは、節の集合からの導出により空節 □ を導くことである。 反駁については以下の定理が成り立つ。
節の集合 S が充足不能である必要十分条件は、節の集合 S からの導出により空節 □ が導けることである。
これはエルブランの定理を導出に応用したものになっている。
論理式 P が恒真であれば ¬ P {\displaystyle \lnot P} は充足不能(恒偽)であるため、節の集合に ¬ P {\displaystyle \lnot P} を追加し導出を繰り返すことで空節 □ になれば、論理式 P が恒真であることが証明できる。
反駁により P {\displaystyle P} が P 1 , ... , P n {\displaystyle P_{1},\dots ,P_{n}} の論理的帰結か調べるアルゴリズムは以下のように表現できる。
P 1 , ... , P n {\displaystyle P_{1},\dots ,P_{n}} をスコーレム連言標準形 C 1 , ... , C n {\displaystyle C_{1},\dots ,C_{n}} に変換する。
¬ P {\displaystyle \lnot P} をスコーレム連言標準形 C {\displaystyle C} に変換する。
もし C , C 1 , .
一般に論理式 F 1 , F 2 {\displaystyle F_{1},F_{2}} を等しくする代入を F 1 , F 2 {\displaystyle F_{1},F_{2}} の単一化子(unifier)といい、そのうち最も一般的な単一化子(最汎単一化子)を F 1 , F 2 {\displaystyle F_{1},F_{2}} のmgu(most general unifier)という。上記の例の場合、両方の論理式を等しくする代入は { z / a , y / f ( b ) , x / a } {\displaystyle \left\{z/a,y/f(b),x/a\right\}} 、 { z / x , y / c , f ( b ) / c } {\displaystyle \left\{z/x,y/c,f(b)/c\right\}} など無数に存在する。これらは本来の代入 { z / x , y / f ( b ) } {\displaystyle \left\{z/x,y/f(b)\right\}} に { x / a } {\displaystyle \left\{x/a\right\}} などの代入を合成したものなので、最汎単一化子 mgu は { z / x , y / f ( b ) } {\displaystyle \left\{z/x,y/f(b)\right\}} である。
導出とは二つの節より新しい節を導き出す操作で、一方の節に含まれるリテラル l {\displaystyle l} と、他方の節に含まれる否定リテラル ¬ l {\displaystyle \neg l} をのぞき、その他のリテラルの論理和をとることで、新しい節を得ることをいう。
命題論理での導出規則を式で表せば、 l ∨ P , ¬ l ∨ Q P ∨ Q {\displaystyle {\frac {l\vee P,\quad \neg l\vee Q}{P\vee Q}}} と書ける。ここで上式は前提となる親節、下式はそれらから導かれる導出節(resolvent)を表す。
あるいは、別の表記法を用いて次のようにも表現できる。前提となる節を C 1 {\displaystyle C_{1}} と C 2 {\displaystyle C_{2}} とし, もしリテラル L ∈ C 1 {\displaystyle L\in C_{1}} と否定リテラル L ̄ ∈ C 2 {\displaystyle {\overline {L}}\in C_{2}} が存在するならば、導出節 C R {\displaystyle C_{R}} は以下のようになる。
C R = ( C 1 ∖ { L } ) ∪ ( C 2 ∖ { L ̄ } ) {\displaystyle C_{R}=(C_{1}\setminus \{L\})\cup (C_{2}\setminus \{{\overline {L}}\})}
導出規則は三段論法や前件肯定を一般化した規則となっている。 導出は完全な証明系であることが知られている。