目次

1. 論理式の標準形

2. 標準形への同値変形

3. 恒真性・充足可能性との関係

4. 導出原理の考え方

総目次に戻る

1. 論理式の標準形

の形に表わしたものに似ている．分配律などを見れば わかるように，もともと選言（論理和）と連言（論理積） を通常の数の和と積に対応させて考えることは不自然 ではない．実際，上のような数式の表示で積 * を連言∧に， 和 + を選言∨に読み替えれば，得られるものは 選言標準形と呼ばれるものに他ならない．

ただし，数式と論理式では大きな違いが一つある． すなわち，和・積と違って選言と連言の役割は完全に対等で， それを入れ替えてもさまざまな性質は変わらない （ド・モルガンの法則や分配律を思い出してみられたい）． このことを双対性（そうついせい）という． この双対性があるために，上のような数式の表示で積を 選言に，和を連言に読み替えた形の表現も可能になる． それが連言標準形である．

1.1 連言標準形

【定義】

1. 原子式または原子式の否定 をリテラルという．
2. 有限個のリテラル L₁, ..., L_k を ∨で結んだ形の論理式 L₁∨…∨L_k を節（あるいは∨節）という．
3. 有限個の節 C₁, ..., C_n を∧で結んだ形 C₁∧…∧C_nを 連言標準形（あるいは論理積標準形）と呼ぶ．

要するに，連言標準形の論理式は

（L₁₁, L₁₂, ... はリテラル） という形をしている．

【例】a1, a2, a3 を原子論理式とするとき， (a1∨¬a2)∧(a1∨¬a3) は連言標準形の論理式である．

【注意】

1. 標準形を考えるときには原子式に命題定数を含めない， という流儀もある．

2. 命題変数と言わずに敢えて「原子式」と言うのは， 原子式の定義を適当に変えれば，この定義が述語論理でも 通用するからである．同じことは後で述べる選言標準形に ついても言える．

1.2 選言標準形

すなわち，リテラルを∧で結んだもの （双対節あるいは∧節と呼ぶ） をさらに∨で結んで得られる形

（L₁₁, L₁₂, ... はリテラル） が選言標準形である．

【注意】ここでいう双対節を「節」と呼ぶこともある． より一般には，有限個のリテラルの集合 {L1, ..., Lk} を 「節」と呼び，状況に応じてそれを∧あるいは∨で結合する， という流儀もある．

1.3 双対性定理

【定義】論理式φが原子式から∧，∨，¬のみによって 構成されているとする．このときφに含まれる∧を∨に， ∨を∧に置き換えて得られる論理式をφ^Dと表わす （D は「双対」にあたる英単語の「dual」の頭文字である）．

【例】a, b, c, d を原子式とするとき， φ = (¬(a∧b)∨¬(c∧d))∧(a∨c) に対して φ^D = (¬(a∨b)∧¬(c∨d))∨(a∧c) となる．

【定義】 原子式 a₁,... , a_nを含む論理式φに対して， それらを別の論理式 ψ₁,... , ψ_n に置き換えて得られる論理式を

とあらわす．

【注意】 この場合に限らず，記号論理学や計算機科学では このように斜線で置き換えを表わす記法が一般的に用いられている．

連言標準形と選言標準形が¬によって互いに移り合うことは， 次のより一般的な結果からの帰結である．

【定理】 論理式φは原子式 a₁, ..., a_n から∧，∨，¬のみで構成されているとする．このとき

となる．

【標準形との関係】論理式φが連言標準形のとき

は選言標準形の論理式であるが，上の定理によれば これは¬φと同値である．このようにして，φに対する 連言標準形と¬φに対する選言標準形は１対１に対応する．

次の小節でこの定理の証明を行う．証明は数学的帰納法の一種である 構造帰納法による．これは論理式の「帰納的定義」 に基づく帰納法で，この場合に限らず数理論理学や計算機科学では 至るところで用いられる基本的な論法である．

論理式が具体的に与えられれば，ド・モルガンの法則を 反復適用し，最後に原子式の二重否定を除去する，という 同値変形によって，定理の主張を確かめることができる．

【例】

1.4 双対性定理の証明

論理結合子を含まない場合にはφ は原子論理式なので， 定理の主張はすぐに確かめられる．そこで，φ における 論理結合子の総数が n 未満の場合に定理が成り立つと仮定して， 論理結合子の総数が n (＞ 0) の場合を考える． φ は φ1∧φ2，φ1∨φ2，¬ψ（φ1, φ2, ψは部分論理式） のいずれかの形に表せる（ここで論理式の帰納的定義を用いる）． φ に含まれる原子式は a₁, ..., a_n である とする．

1.φ = φ1∧φ2 の場合

ド・モルガンの法則と双対論理式の定義によって

¬φ ≡ (¬φ1)∨(¬φ2), 　 φ^D = φ1^D∧φ2^D

となるが，φ1とφ2では論理結合子の数がφよりも 少なくとも１だけ少ないので，帰納法の仮定が使えて

¬φ1 ≡ φ1^D[¬a₁／a₁, ..., ¬a_n／a_n],
¬φ2 ≡ φ2^D[¬a₁／a₁, ..., ¬a_n／a_n]

となる．これを上の式に代入すると

.

¬φ	≡	φ1D[¬a1／a1, ..., ¬an／an] ∨ φ2D[¬a1／a1, ..., ¬an／an]
	≡	(φ1∧φ2)D[¬a1／a1, ..., ¬an／an]
	≡	φD[¬a1／a1, ..., ¬an／an]

となって，φについても定理の主張が成り立つことがわかる．

2.φ = φ1∨φ2 の場合

1 とまったく同様である（各自確認のため自分でやり直して みよ）．

3.φ = ¬ψ の場合

定義に戻って考えれば φ^D = ¬(ψ^D) なので

φ^D[¬a₁／a₁, ..., ¬a_n／a_n] = ¬(ψ^D[¬a₁／a₁, ..., ¬a_n／a_n])

となるが，ψには帰納法の仮定が使えて

¬ψ = ψ^D[¬a₁／a₁, ..., ¬a_n／a_n]

であるから，

φ^D[¬a₁／a₁, ..., ¬a_n／a_n] ≡ ¬(¬ψ) ≡ ψ ≡ ¬φ

となって，φ に対して定理の主張が成り立つ．

1.4 ブール函数との関係

任意のブール函数は論理式として表現することができる． このことを示す際に選言・連言標準形が現れる．

【定理】0, 1 を F, T と同一視するとき，任意のブール 函数は x₁, ..., x_n を命題変数 とする論理式で表現できる．正確に言えば， {0,1}ⁿ の部分集合 I, J を

で定義するとき（したがって f = χ_I, ¬f = 1 - f = χ_Jとなる），f は次のような 標準形の論理式で表現できる：

1. 連言標準形による表示
   f(x₁, ..., x_n) = ∨_{(b1,...,bn)∈I} (L₁(b₁)∧ ... ∧L_n(b_n))

2. 連言標準形による表示
   f(x₁, ..., x_n) = ∧_{(b1,...,bn)∈J} (¬L₁(b₁)∨ ... ∨¬L_n(b_n))

というように定めたリテラルである．また， ∧_{(b1,...,bn)∈J} は J の要素全体にわたって，対応する論理式の連言を とることを意味する． ∨_{(b1,...,bn)∈I} も同様の意味である．

【証明】選言標準形の場合がわかりやすいので，そちらを 説明する．選言標準形については，¬f を選言標準形で 表わしてから， 双対により f に戻せばよい． L₁(b₁)∧ ... ∧L_n(b_n)) という論理式の 真理値は (x₁, ..., x_n) = (b₁, ..., b_n) のときのみ T, それ以外では F である．したがってそれらの (b₁, ..., b_n) ∈J にわたる選言は (x₁, ..., x_n) の値が I に属するとき値 T,そうでないとき値 F をとる． これは f の真理値と一致するので， 両者は {0,1}ⁿ の函数として一致する （証明終わり）．

【例】次のような表で定義されるブール函数 f(x1,x2,x3) を考える．

函数 f: {0,1}³ --> {0,1}

x1	x2	x3	f(x1, x2, x3)
1	1	1	0
1	1	0	1
1	0	1	1
1	0	0	1
0	1	1	0
0	1	0	0
0	0	1	0
0	0	0	1

この函数は次のように表示できる：

命題論理の任意の論理式 φ が与えられたとき， 命題変数をブール変数と読み替えることによって ブール函数 f が決まる．上の定理を適用すれば， このブール函数を連言・選言標準形に表わせる． 論理式に戻って考えれば，これは φ と論理的に同値な 連言・選言標準形の論理式を求めたことに他ならない． こうして，上の定理の系として，任意の論理式に対する 同値な標準形の論理式の存在がわかる：

【系】任意の論理式φに対して， それと同値な連言・選言標準形の論理式が存在する．

ブール函数の標準形の存在定理は三種類の基本的な演算 ∧，∨，¬ の組み合わせによってどのようなブール函数も表現できるということを 示している．これは論理回路の物理的設計という観点から見ても 極めて重要な結果である．この定理のおかげで，三種類の演算に対応する 論理素子（ゲート）とそれを組み合わせる方法さえ用意しておけば， どのような論理回路も実現することができるのである．

ただし，なるべく少ない論理素子で回路を実現したい， という効率上の観点から見れば，このような標準形は無駄が多い． 効率の良い論理回路の設計にはまったく別の考え方が必要になる．

なお，この三種類の基本演算をさらに

1. ¬(x∧y) （NAND）
2. ¬(x∨y) （NOR）

【演習問題】x∧y, x∨y, ¬x を NAND（あるいは NOR）で表わせ （ヒント：まず ¬x を実現することから考えてみよ）．

2. 標準形への同値変形

2.1 連言標準形への同値変形

第一段階

与えられた論理式に対して→と↔の書き換え公式

φ1→φ2	≡	(¬φ1)∨φ2
φ1↔φ2	≡	(φ1→φ2)∧(φ2→φ1)

を適用し，∧と∨と¬のみ含む論理式に同値変形する．

第二段階

第一段階で得られた論理式に対してド・モルガンの法則と 二重否定の除去の公式を適用し，リテラルを∧と∨で結んだ形の 論理式に同値変形する．正確に言えば，

• φ = ¬(φ1∧φ2) のとき，それと同値な (¬φ1)∨(¬φ2) に置き換える
• φ = ¬(φ1∨φ2) のとき，それと同値な (¬φ1)∧(¬φ2) に置き換える
• φ = ¬¬ψ のとき，それと同値なψに置き換える

という操作を，与えら得た論理式から出発して，部分論理式に 対して繰り返す．

第三段階

第二段階で得られた論理式に対して分配律

φ1∨(φ2∧φ3)	≡	(φ1∨φ2)∧(φ1∧φ3)
(φ1∧φ2)∨φ3	≡	(φ1∨φ3)∧(φ2∨φ3)

を反復適用し，すべての∨をリテラルの直前に移動する． ただし，分配律の基本形を反復して使うのは煩わしいので， それを複合して得られる公式

(φ₁∧…∧φ_m)∨ (ψ₁∧…∧ψ_n) ≡ (φ₁∨ψ₁)∧…∧ (φ₁∨ψ_n)∧…∧ (φ_n∨ψ₁)∧…∧ (φ_n∨ψ_m)
= ∧_{1≦i≦m, 1≦ｊ≦n} (φ_i∨ψ_j)

などで一気に処理してもよい．ただし最後の記号は 1 ≦ i ≦ m, 1 ≦ j ≦ n という mn 個の添字対 (i,j) にわたって∧をとることを意味する． 慣れないうちは

∧ ----> +, 　∨ ----> *

という読み替えで数式に翻訳し，数式の単項式への 展開と思って計算するのがわかりやすい．

2.2 連言標準形への同値変形の例

【例】¬a1→¬(a2∨a3)（a1, a2, a3 は原子式） を連言標準形に同値変形する：

この計算例ではほとんどの部分が→と¬の処理で， 最後に１回だけ分配律を使っている．

【例】(a1∧a2)∨(a3∧(a4∨(a5∧a6))) （a1, ..., a5 は原子式）を連言標準形に同値変形する：

この例では前述の「第三段階」のみが問題である． 計算例に示したように，一番内側の括弧 (...) から外側へ 向かって連言標準形を順次成長させて行けば，自然に同値変形 が完成する．

よくわからない場合は ∧----> +, ∨----> * という置き換えを行って 得られる数式 (a1 + a2)*(a2 + (a4 * (a5 + a6))) の展開を参考にすること．

【例】modus ponens を表わす式 (a1∧(a1→a2))→a2（a1, a2, a3 は原子式） を連言標準形に同値変形する：

a1∨¬a1 ≡ T, a2∨¬a2 ≡ T （言い替えればa1∨¬a1, a2∨¬a2 は恒真式）なので，ここで得られた連言標準形は a1, a2, a3 の任意の真理値割り当てに対して常に真である．したがって この例（modus ponens を表わす）は恒真式であることが わかる．このように，連言標準形を見れば恒真式であるか どうかはただちに判断できる（このことはあとで一般的に 議論する）．

2.3 選言標準形への同値変形

第三段階

第二段階で得られた論理式に対して分配律

φ1∧(φ2∨φ3)	≡	(φ1∧φ2)∨(φ1∧φ3)
(φ1∨φ2)∧φ3	≡	(φ1∧φ3)∨(φ2∧φ3)

を反復適用し，すべての∧をリテラルの直前に移動する． ここでも分配律を複合して得られる公式

(φ₁∨…∨φ_m)∧ (ψ₁∨…∨ψ_n) ≡ (φ₁∧ψ₁)∨…∨ (φ₁∧ψ_n)∨…∨ (φ_n∧ψ₁)∨…∨ (φ_n∧ψ_m)
= ∨_{1≦i≦m, 1≦ｊ≦n} (φ_i∧ψ_j)

などで一気に処理してもよい（最後の記号の 意味は連言標準形への同値変形のところで 説明したものと同様）．また，ここでも

∨ ----> +, 　∧ ----> *

という読み替えで数式に翻訳し，数式の単項式への 展開と思って計算するのがわかりやすい．

【演習問題】連言標準形への同値変形の例として 採り上げた論理式を，今度は選言標準形に同値変形 すること．

2.4 標準形の存在定理

【定理】任意の論理式は以上のような手続きによって 連言・選言標準形に同値変形できる．

この定理が正しいことはさまざまな計算例や 通常の数式の計算からの類推で納得できるだろう． 厳密な証明は構造帰納法によって行えばよい． これは演習問題として各自に任せる．

【演習問題】上の定理を証明せよ．第一段階の変形は明らかなので， 第二・第三段階の変形ができることを示せばよい．具体的には， 論理式に含まれる∧，∨，¬の総数についての数学的帰納法に 持ち込む．

3. 恒真性・充足可能性との関係

3.1 連言標準形と恒真性

与えられた論理式が連言標準形

（C₁, ..., C_m は節，すなわち リテラルの選言）に同値変形されたとする．引き続いて， 各節の中で

• 同じリテラル L が L∨L の形で現れるときには， それらを L に置き換える

• 同じ原子式が a∨¬a の形で現れるときには， それを含む連言自体を T で置き換える

以上の考察から，恒真性に関して次のような判定法が得られる．

【連言標準形による恒真性の判定】 論理式φを連言標準形に同値変形し，さらに 各節を a∨a, ¬a∨¬a, a∨¬a（a は原子式） という部分論理式を含まないように同値変形する． このとき

1. φが T のみからなる論理式に帰着すれば， φ は恒真式である．

2. そうでなければ，φは恒真式ではない．

【例】すでに示した計算例の中のmodus ponensの論理式 の連言標準形を考える：

上に述べたような変形によって，上式右辺の連言標準形は 次のように同値変形される：

残ったものは T のみである．したがってもとの論理式が 恒真式であることがわかる．

【例】((a1∧a2)→¬(a3∧a4)∧(a1∨a3) を同値変形して 得られる連言標準形 (¬a1∨¬a2∨¬a3∨¬a4)∧(a1∨a3) を考える．適当な真理値割り当て M に対してここに現れた二つの節の いずれかが F であれば標準形は F となり，論理式が恒真でない ことがわかる．実際，(¬a1∨¬a2∨¬a3∨¬a4) と (a1∨a3) は それぞれ

および

という真理値割り当て M に対して F の値をとる．

【演習問題】前章で示したさまざまな恒真式の恒真性を 上の方法で再確認せよ．

3.2 選言標準形と充足問題

【選言標準形による充足問題の解法】 論理式を選言標準形

（D₁, ..., D_m は双対節， すなわちリテラルの連言）に同値変形する．さらに， 各双対節を a∧a, ¬a∧¬a, a∧¬a（a は原子式） という形の部分論理式を含まない形に同値変形する． このとき

1. φ が F のみからなる論理式に帰着すれば， φ は充足不可能である．

2. そうでなければ，F に帰着しないで残る 双対節のそれぞれから充足問題の（少なくとも） 一つの解が得られる．

（L_j = p_j または ¬p_j） である．それに対して真理値割り当て M を

というように選ぶことができる（すべての原子式がそこに 現れていれば M は一意的に定まるが，そうでなければ， そこに現れない原子式には任意の値を割り当ててよい）． このような真理値割り当て M はφを充足する．

【例】「箱とボールのパズル」を選言標準形の応用として 扱ってみよう．たとえば

1. 箱ＡにもＢにもボールが入っていれば， 箱Ｃには入っていない．
2. 箱Ａにボールが入っていなければ， 箱Ｂか箱Ｃのいずれかにはボールが入っている．

1. M[a] = F, M[b] = T, M[c] = 任意
2. M[a] = F, M[b] = 任意, M[c] = T
3. M[a] = F, M[b] = F, M[c] = 任意
4. M[a] = 任意, M[b] = F, M[c] = T
5. M[a] = T, M[b] = 任意, M[c] = F
6. M[a] = 任意, M[b] = T, M[c] = F

【演習問題】 ある電子装置には四つの付属品 a,b,c,d が付属している． この付属品は本体に用意された端子に接続して使う．ただし， 接続するときには次の条件をすべて満たさなければならない：

1. a を接続しないときには b と c の両方を接続しなければ ならない．
2. b を接続しないときには c か d のいずれか（両方でもよい） を接続しなければならない．
3. a と d を同時に接続することはできない．

【注意】実際にやってみればわかることであるが， この問題を選言標準形への同値変形で解くことは 非常に手間がかかる．特に，各双対節は一般には 複数の解をもち，双対節間に解の重複があり得るが， この重複を除くには解を列挙してみるしかない． これでは何のために標準形を求めたのかわからない． 2⁴ = 16 通りの場合から条件に該当しないものを 順次を消して行く，という原始的なやり方の方が かえって速く答が出せる．このような意味で， 標準形を利用する方法は充足問題の解法として 決して効率が良いとは言えない．

4. 導出原理の考え方

【注意】「resolution principle」は「導出原理」と訳されることが多いので ここでもこの訳語を採用するが，「resolution」を「導出」と訳すのは あまり適切ではない．むしろ「分解」あるいは「解消」という言葉の方が 本来の意味に近い．そこで，用語として不統一ではあるが，ここでは 「resolution」に「解消」という言葉を充てることにした．

4.1 導出原理による恒真性の判定

まず「解消」の定義から始める．

【定義】

1. 双対節 D, D' がある命題変数 p とその否定 ¬p を
   D = p∧A₂∧…∧A_m （A₂, ..., A_mはリテラル）, D' = ¬p∧B₂∧…∧B_n （B₂, ..., B_nはリテラル）

   という形で含むとする．これらから

   D'' = A₂∧…∧A_m∧B₂∧…∧B_n

   という新たな双対節をつくることをD∨D'から p,¬p の対を解消する という．この操作を記号的に

   D∨D' 〜＞ D''

   と表わす（これはここだけの記号である）．ただし， D'' の中に同じリテラル L が重複して現れたら， それを一つにまとめたものを改めて D'' とする （この修正を忘れると誤った結果を生じるので注意）． また，D = p, D' = ¬p の場合には何も残らないので 便宜的に D'' = T と定義する．

2. 選言標準形の論理式 φ = D₁∨…∨D_n の中の一対の双対節 D_i, D_j に対して 上のような解消操作 D_i∨D_j 〜> D'' を行って新たな選言標準形の論理式 φ'' が得られることを，記号的に
   φ 〜> φ''

   と表わす（これもここだけの記号である）．たとえば i=1, j=2 のときには

   φ = D₁∨D₂∨…∨D_n 〜> φ'' = D'' ∨D₃∨…∨D_n

   となる．ただし，φ'' の中に同じ双対節 D が 重複して現れたら， それらを一つにまとめたものを改めて φ'' とする． D'' = T のときには（φ'' ≡ T なので）それ以上の解消操作はしない．

選言標準形で与えられた任意の論理式φは上の操作の繰り返し

によって，それ以上解消ができないか，あるいは T と同値な， ある論理式φ_Nに到達する． このような解消列の選び方は一般には複数通り可能である．

【例1】φ = (p∧r)∨(¬p∧q∧s)∨(¬q∧p∧t) （p,q,r,s は命題変数）に対しては次の三通りの解消が可能である （これ以外にはない）．

その１：

(p∧r)∨(¬p∧q∧s)∨(¬q∧p∧t)

〜> (r∧q∧s)∨(¬q∧p∧t)　(最初の二つの双対節から p,¬p を解消）

〜> r∧s∧p∧t　（q,¬q の対を解消）

その２：

(p∧r)∨(¬p∧q∧s)∨(¬q∧p∧t)

〜> (p∧r)∨(¬p∧s∧p∧t)　（最後の二つの双対節から q,¬q を解消）

〜> r∧s∧p∧t 　（p,¬q を解消）

その３：

(p∧r)∨(¬p∧q∧s)∨(¬q∧p∧t)

〜> (p∧r)∨(q∧s∧¬q∧t) 　（最後の二つの双対節から p,¬p を解消）

【例2】φ = (p∧¬q)∨(q∧¬r)∨(r∧p)∨¬p （p,q,r は命題変数）についても同様に複数の解消の仕方が可能であるが， その中には T に到達するものがある．たとえば左から順次解消操作を行えば

(p∧¬q)∨(q∧¬r)∨(r∧p)∨¬p

〜> (p∧¬r)∨(r∧p)∨¬p　（q,¬q を解消）

〜> p∨¬p　（r,¬r を解消，重複して現れた p を一つにまとめる）

〜> T 　（p,¬p を解消）

恒真性判定の基礎となるのは次のことである．

【定理】φ 〜> φ'' かつ φ'' が恒真ならばφも恒真である．

定理の証明のために次の穂題を用意する．

【補題】二つの双対節 D, D' に対して D∨D' 〜> D'' とする． また，M をD, D' に含まれる命題変数の任意の真理値割り当て M とする． このとき M[D''] = T ならば M[D∨D'] = T である．

【証明】D, D' を D = p∧C, D' = ¬p∧C'（C, C' は双対節） というように表わせば D'' = C∧C' である． M[p] の値について場合分けして考える．

1. M[p] = T のとき： M[D] = M[C], M[D'] = F であり， したがって M[D∨D'] = M[C] となる．
2. M[p] = F のとき：M[D] = F, M[D'] = M[C'] であり， したがって M[D∨D'] = M[C'] となる．

【定理の証明】φ = D₁∨D₂∨ψ, φ'' = D''∨ψ, D₁∨D₂ 〜> D'' （ψは D₁, D₂, D'' 以外の双対節の 選言をまとめて表わしたもの）という設定で考えればよい． 例外的に φ = D₁∨D₂ となる場合は 別途考えればよいので，ここでは省略する（各自に任せる）． φに含まれる命題変数に対する任意の真理値割り当て M を考える． 仮定によって φ'' は恒真であるから M[φ''] = T となる． このとき M[D''] = T あるいは M[ψ] = T となる． M[D''] = T ならば補題によって M[D∨D'] = T となるから， M[φ] = T である．M[ψ] = T ならば D∨D' の真理値と 無関係に M[φ] = T である．いずれにせよ M[φ] = T となる． 任意の真理値割り当てに対してこれが成立するから，φも恒真である． （証明終わり）

このことから，次のような恒真性の判定法がわかる．

【系】φから T と同値な論理式に至る解消操作

が存在すれば，φは恒真である．

【証明】定理によれば，恒真式 φ_N ≡ T から出発して 逆向きにたどることによって φ_N-1, φ_N-2, ... の恒真性が順次従う．（証明終わり）

【注意】実はこの系の逆も成立する．すなわち，φが恒真ならば T と同値な論理式に到達する解消操作が必ず存在する （導出原理の完全性）． 証明には手間がかかるのでここでは省略する．

【例】すでに示した解消操作の結果から， (p∧r)∨(¬p∧q∧s)∨(¬q∧p∧t) は恒真ではないが， (p∧¬q)∨(q∧¬r)∨(r∧p)∨¬p は恒真である， ということがわかる．ちなみに，後者の恒真性は p, q, r の真理値について適当な順序で場合分けすることによっても 確かめられるが，上の補題の証明からわかるように， 解消によって恒真性を判定する方法の裏にはそのような 場合分けの考え方が隠れている．

【注意】恒真であることを示すには T と同値な論理式への解消が 一つでも見つかれば十分だが，どのようにしてそれを見つけるかは 別問題である．また，恒真でないことを示すには（上の系に基づく限り） どの解消も T に同値な論理式に到達しないことを確かめなければならない． ここではこれらの点を改善する議論には立ち入らない．

4.2 導出原理による充足不可能性の判定

恒真性の判定の出発点となるのは選言標準形であるから， 充足不可能性の判定ではその双対である連言標準形の 論理式 C₁∧…∧C_n （各 C_i は節）から出発する． 解消操作も以下のように∧と∨を入れ換えた形になる．

【定義】

1. 節 C, C' がある命題変数 p とその否定 ¬p を
   C = p∨A₂∨…∨A_m （A₂, ..., A_mはリテラル）, C' = ¬p∨B₂∨…∨B_n （B₂, ..., B_nはリテラル）

   という形で含むとする．これらから

   C'' = A₂∨…∨A_m∨B₂∨…∧B_n

   という新たな節をつくることをC∧C'から p,¬p の対を解消する という．この操作を記号的に

   C∧C' 〜> C''

   と表わす（これはここだけの記号である）．ただし， C'' の中に同じリテラル L が重複して現れたら， それを一つにまとめたものを改めて C'' とする （この修正を忘れると誤った結果を生じるので注意）． また，C = p, C' = ¬p の場合には何も残らないので 便宜的に C'' = F と定義する．

2. 選言標準形の論理式 φ = C₁∧…∧C_n の中の一対の双対節 C_i, C_j に対して 上のような解消操作 C_i∧C_j 〜> C'' を行って新たな選言標準形の論理式 φ'' が得られることを，記号的に
   φ 〜> φ''

   と表わす（これもここだけの記号である）．たとえば i=1, j=2 のときには

   φ = C₁∧D₂∧…∧D_n 〜> φ'' = C''∧C₃∧…∧C_n

   となる．ただし，φ'' の中に同じ節 C が 重複して現れたら， それらを一つにまとめたものを改めて φ'' とする． C'' = F のときには（φ'' ≡ F なので）それ以上の解消操作はしない．

連言標準形の論理式に対する解消操作をこのように定義するとき， 恒真性の判定の場合と同様にして以下のことが証明できる （証明は演習問題として各自に任せる）．

【補題】二つの節 C, C' から解消によって節 C'' が得られるとする． また，M を C, C' に含まれる命題変数の任意の真理値割り当てとする． このとき M[C∧C'] = T ならば M[C''] = T である．

【定理】φ〜> φ'' かつφが充足可能ならばφ''も充足可能である．

【系】φから F と同値な論理式に至る解消操作

が存在すれば，φは充足不可能である．

【注意】この系の逆も成立する．すなわち，φが充足不可能ならば F と同値な論理式に到達する解消操作が必ず存在する． これも「導出原理の完全性」と呼ばれる（証明は省略する）．

結論として，F と同値な論理式への解消が一つでもあればφは充足不可能であり， また，どの解消も F に到達しなければφは充足可能である， ということになる．

4.3 通常の定式化との関係

{{p,¬q}, {q,¬r}, {r,p}, {¬p}}

〜> {{p,¬r}, {r,p}, {¬p}}　（q,¬q を解消）

〜> {{p},{¬p}}　（r,¬r を解消）

〜> {{ }} 　（p,¬p を解消）

このような定式化では，リテラルの集合としての節を どのように解釈するかはあらかじめ特定されておらず， 解釈を決めることによってその意味が決まる．すなわち

1. {L₁,… , L_n} を L₁∧…∧L_n， 空節 { } を T と解釈すれば，導出原理は 選言標準形の論理式の恒真性を判定する手続きとなる

2. {L₁,… , L_n} を L₁∨…∧∨_n， 空節 { } を F と解釈すれば，導出原理は 連言標準形の論理式の充足不可能性を判定する手続きとなる

解消の概念は論理式の演繹関係（|= あるいは |-） と密接な関係があるが，選言標準形の場合と 連言標準形の場合では微妙な違いがある．すなわち， 選言標準形の解消は演繹関係と逆向きになる （すなわち φ〜>φ' ならば φ'|=φ）が， 連言標準形の解消は同じ向きである （すなわち φ〜>φ' ならば φ|=φ'）．この意味で， 連言標準形の解消は「形式的推論」（あるいは 「形式的演繹」）の一種と考えることができる． これは「形式化された論理」の一例である （論理の形式化については後の章で詳しく説明する）．

キーワード