論理的同値性と 命題論理式の同値変形

2020 年度 数理論理学 講義資料 (4)

青戸 等人

(

知能情報システムプログラ ム

)

目次

-

論理的同値性と 命題論理式の同値変形

-

標準形と 標準形の構成

論理的同値性

定義

4.1. A, B

を 命題論理式と する ． 任意の付値

v

_につい て，

[[A]]_v = [[B]]_v

と なる と き ，

A

_と

B

_{は 論理的同値である と} いい，

A ∼= B

_{と 書く ．}

命題論理式の論理的同値性は真理値表を 用いて チェッ ク でき る ．

例

4.2. ¬(P ∨ Q) ∼= ¬P ∧ ¬Q

P Q P ∨ Q ¬(P ∨ Q) ¬P ¬Q ¬P ∧ ¬Q

T T T F F F F

T F T F F T F

F T T F T F F

F F F T T T T

演習

4.3.

真理値表を 用いて ，

P → Q ∼= ¬Q → ¬P

を 確かめよ ．

P Q P → Q ¬Q ¬P ¬Q → ¬P

T T T F F T F F

演習

4.4.

(

真理値表ではなく

)

解釈の定義を 用いて ，

¬(P ∧ Q) ∼= ¬P ∨

¬Q

である こ と を 示せ．

演習

4.3.

真理値表を 用いて ，

P → Q ∼= ¬Q → ¬P

を 確かめよ ．

P Q P → Q ¬Q ¬P ¬Q → ¬P

T T T F F T

T F F T F F

F T T F T T

F F T T T T

演習

4.4.

(

真理値表ではなく

)

解釈の定義を 用いて ，

¬(P ∧ Q) ∼= ¬P ∨

¬Q

である こ と を 示せ．

(

解答例

)

[[¬(P ∧ Q)]]_v = T ⇔ [[P ∧ Q]]_v = F

⇔ [[P]]_v = F

ま たは

[[Q]]_v = F

⇔ [[¬P]]_v = T

ま たは

[[¬Q]]_v = T ⇔ [[¬P ∨ ¬Q]]_v = T

注意

!

注意

!

注意

!

=

と

∼=

は異なる

“A = B”

の意味は， 命題論理式

A

_{と 命題論理式}

B

_{はま っ} たく 同じ 形， と いう こ と ．

一方，

“A ∼= B”

の意味は， 命題論理式

A

_{と 命題論理式}

B

が論理的同値， と いう こ と ． つま り ，

A

_と

B

_{の形は違っ ても} よ い．

例．

P → Q ∼= ¬Q → ¬P

_{ではある が，}

P → Q 6= ¬Q → ¬P (

つま

り ，

P → Q = ¬Q → ¬P

ではない

)

．

ト ート ロジー・ 充足可能性と 論理的同値性の関係

ト ート ロジー・ 充足可能性と 論理的同値性の間には以下 に示すよ う な関係がある ． 証明は容易なので省略．

(1) A

がト ート ロジーかつ

A ∼= B =⇒ B

_{がト ート ロジー}

A

_{が充足可能かつ}

A ∼= B =⇒ B

_{が充足可能}

(2) A ∼= B ⇐⇒ A ↔ B

_{がト ート ロジー}

(3) A

_{がト ート ロジー}

⇐⇒ A ∼= ⊤

¬A

_{がト ート ロジー}

⇐⇒ A ∼= ⊥

重要な同値式 (1)

以下に重要な同値式を 示す．

A, B, . . .

_{は任意の命題論理} 式を 表わす．

巾等律

A ∧ A ∼= A A ∨ A ∼= A

交換律

A ∧ B ∼= B ∧ A A ∨ B ∼= B ∨ A A ↔ B ∼= B ↔ A

結合律

(A ∧ B) ∧ C ∼= A ∧ (B ∧ C) (A ∨ B) ∨ C ∼= A ∨ (B ∨ C)

分配律

A ∧ (B ∨ C) ∼= (A ∧ B) ∨ (A ∧ C) (A ∨ B) ∧ C ∼= (A ∧ C) ∨ (B ∧ C) A ∨ (B ∧ C) ∼= (A ∨ B) ∧ (A ∨ C) (A ∧ B) ∨ C ∼= (A ∨ C) ∧ (B ∨ C)

吸収律

A ∧ (A ∨ B) ∼= A A ∨ (A ∧ B) ∼= A

ド ・ モルガン の法則

¬(A ∧ B) ∼= ¬A ∨ ¬B

¬(A ∨ B) ∼= ¬A ∧ ¬B

二重否定の法則

¬¬A ∼= A

対偶

A → B ∼= ¬B → ¬A

同値の法則

A ↔ B ∼= (A → B) ∧ (B → A)

含意の法則

A → B ∼= ¬A ∨ B

重要な同値式 (2)

⊤

と

⊥

に関する 以下のよ う な同値式も 重要．

⊥

規則

/⊤

規則

A ∧ ¬A ∼= ⊥ A ∨ ¬A ∼= ⊤

¬⊤ ∼= ⊥ ¬⊥ ∼= ⊤ A ∧ ⊥ ∼= ⊥ A ∧ ⊤ ∼= A A ∨ ⊥ ∼= A A ∨ ⊤ ∼= ⊤ A → ⊥ ∼= ¬A ⊤ → A ∼= A

論理的同値性の性質

定理

4.5.

論理的同値性は命題論理式集合上の合同関係．

合同関係と は

(

復習

)

同値関係

(

反射的， 推移的， 対称的な関係

)

で， さ ら に以 下を 性質を 満たす：

(1) A ∼= B ⇒ ¬A ∼= ¬B

_，

(2) A ∼= B

_かつ

C ∼= D ⇒ A ∧ C ∼= B ∧ D

_，

(3) A ∼= B

_かつ

C ∼= D ⇒ A ∨ C ∼= B ∨ D

_，

(4) A ∼= B

_かつ

C ∼= D ⇒ A → C ∼= B → D

_，

(5) A ∼= B

_かつ

C ∼= D ⇒ A ↔ C ∼= B ↔ D

(1)–(5)

は， 命題論理式のある 部分を 同値なも のに置き

替えて も ， 全体が同値のま ま である こ と を 表わす．

命題論理式の同値変形と は

論理的同値性が合同関係である こ と から ， 論理的同値性 に 同値変形を使う こ と が出来る ． すでにわかっている 同値式

(

本講義では， 資料で与えた「 重要な同値式」 と する

)

を 使っ て ， 部分式を 変形し て 得ら れる も のは論理的同値になる ．

例．

P ∧ Q ∼= ¬(P → ¬Q)

． なぜなら ，

¬(P → ¬Q) ∼= ¬(¬P ∨ ¬Q) (

含意

)

∼= ¬(¬(P ∧ Q)) (

ド ・ モルガン

)

∼= P ∧ Q (

二重否定

)

真理値表によ る チェッ ク は述語論理では適用が難し いが， 同

値変形は述語論理でも 使える ．

演習

4.6.

同値変形を 用いて 以下を 示せ．

(1) P ∧ Q ∼= ¬(¬P ∨ ¬Q) (2) P → ¬R ∼= R → ¬P (3) Q ∧ (Q → P) ∼= P ∧ Q

(1) P ∧ Q ∼= ¬¬(P ∧ Q) (

二重否定

)

∼= ¬(¬P ∨ ¬Q) (

ド ・ モルガン

)

(2) P → ¬R ∼= ¬P ∨ ¬R (

含意

)

∼= ¬R ∨ ¬P (

交換律

)

∼= R → ¬P (

含意

) (

別解

) P → ¬R ∼= ¬¬R → ¬P (

対偶

)

∼= R → ¬P (

二重否定

) (3) Q ∧ (Q → P) ∼= Q ∧ (¬Q ∨ P) (

含意

)

∼= (Q ∧ ¬Q) ∨ (Q ∧ P) (

分配律

)

∼= ⊥ ∨ (Q ∧ P) (⊥

規則

)

∼= Q ∧ P (⊥

規則

)

∼= P ∧ Q (

交換律

)

目次

-

論理的同値性と 命題論理式の同値変形

-

標準形と 標準形の構成

∧ , ∨ の結合律・ 交換律と 括弧の省略

∧

や

∨

の結合律よ り ， 論理的同値性について 考え る 場合は，

(A₁ ∧(A₂ ∧ A₃)) ∧ A₄

_や

A₁ ∧((A₂ ∧A₃) ∧ A₄)

や

A₁ ∧ (A₂ ∧ (A₃ ∧ A₄)))

等は， 区別し ないで，

A₁ ∧ A₂ ∧ A₃ ∧ A₄

_{と 書} いてよ い． 本節ではこ のよ う な

∧

同士，

∨

同士の括弧を 省略 する ．

定義

4.7. n ≥ 1

と する ．

(1) A₁ ∧ · · · ∧ A_n

_を

Vn

i=1 A_i

_{と 書く ．}

(2) A₁ ∨ · · · ∨ A_n

_を

Wn

i=1 A_i

_{と 書く ．} 特に

n = 1

のと き ，

Vn

i=1 A_i = Wn

i=1 A_i = A₁

_{と なる こ と} に注意．

(n = 0

のと き に，

Vn

i=1 A_i = ⊤

，

Wn

i=1 A_i = ⊥

と

おく こ と も ある が， こ こ では

n ≥ 1

と 約束する ．

)

論理積標準形と 論理和標準形

定義

4.8.

(1) P

_{も し く は}

¬P

_{の形の命題論理式を} リ テラ ルと よ ぶ．

(

こ こ で，

P

は命題変数と する ．

)

(2) L₁₁, . . . , L_1n1, . . . , L_m1, . . . , L_mnm(n₁, . . . , n_m, m ≥ 1)

を リ テラ ルと し たと き ，

Vm

i=1

Wn_i

j=1 L_ij

_{を 論理積標準形}

(CNF: conjunctive normal form)

と よ ぶ．

(3) L₁₁, . . . , L_1n1, . . . , L_m1, . . . , L_mnm(n₁, . . . , n_m, m ≥ 1)

を リ テラ ルと し たと き ，

Wm

i=1

Vn_i

j=1 L_ij

_{を 論理和標準形}

(DNF: disjunctive normal form)

と よ ぶ．

例．

(¬Q ∨ P) ∧ (R ∨ ¬Q) ∧ (P ∨ Q ∨ R)

は

CNF

．

( ¬Q

|{z}L₁₁

∨ P

|{z}L₁₂

) ∧ ( R

|{z}L₂₁

∨ ¬Q

|{z}L₂₂

) ∧ ( P

|{z}L₃₁

∨ Q

|{z}L₃₂

∨ R

|{z}L₃₃

)

演習

4.9.

以下の命題論理式が論理積標準形である か， 論 理和標準形である か答えよ ．

(1) (P ∧ Q) ∨ Q ∨ P

(2) (P ∨ Q) ∧ (Q ∨ P ∨ Q) (3) ¬(P ∧ Q) ∨ ¬(Q ∧ P) (4) (¬¬P ∧ ¬Q) ∨ ¬P (5) (Q ∨ P) ∧ ⊥

(6) ((Q ∨ P) ∧ Q) ∨ P (7) P ∨ Q ∨ ¬R

(8) P ∧ Q ∧ ¬R

演習

4.9.

以下の命題論理式が論理積標準形である か， 論 理和標準形である か答えよ ．

(1) (P ∧ Q) ∨ Q ∨ P

論理和標準形

(2) (P ∨ Q) ∧ (Q ∨ P ∨ Q)

論理積標準形

(3) ¬(P ∧ Q) ∨ ¬(Q ∧ P)

ど ち ら でも ない

(4) (¬¬P ∧ ¬Q) ∨ ¬P

ど ち ら でも ない

(5) (Q ∨ P) ∧ ⊥

ど ち ら でも ない

(6) ((Q ∨ P) ∧ Q) ∨ P

ど ち ら でも ない

(7) P ∨ Q ∨ ¬R

論理積標準形かつ論理和標準形

(8) P ∧ Q ∧ ¬R

論理積標準形かつ論理和標準形

(7)

は， 論理積標準形と し て みる と き は，

P

|{z}L₁₁

∨ Q

|{z}L₁₂

∨ ¬R

|{z}L₁₃

と し て 考え

(m = 1

と なる

)

， 論理和標準形と し て みる と き は，

P

|{z}L₁₁

∨ Q

|{z}L₂₁

∨ ¬R

|{z}L₃₁

と

し て 考え

(m = 3, n₁ = n₂ = n₃ = 1

と なる

)

と 考える ．

標準形への同値変形 ( 標準化 )

同値変形に基づく 標準形への変換を 紹介する ．

定理

4.10.

任意の命題論理式

A

_{に対し て，}

A

_{と 論理的同値} な論理積標準形が存在する ． ま た，

A

と 論理的同値な論理和 標準形が存在する ．

例．

¬¬P ∧ Q → ⊥

∼= ¬¬P ∧ Q → P ∧ ¬P (⊥

規則

)

∼= ¬(¬¬P ∧ Q) ∨ (P ∧ ¬P) (

含意

)

∼= ¬¬¬P ∨ ¬Q ∨ (P ∧ ¬P) (

ド ・ モルガン

)

∼= ¬P ∨ ¬Q ∨ (P ∧ ¬P) (

二重否定

) · · · DNF

∼= (¬P ∨ ¬Q ∨ P) ∧ (¬P ∨ ¬Q ∨ ¬P) (

分配律

) · · · CNF

(

証明

)A

と 論理的同値な論理積標準形・ 論理和標準形を 以下 のよ う にし て 構成する ．

(Step 1)

適当な命題変数

P

_{を 選び，}

⊥ ∼= P ∧ ¬P

_，

⊤ ∼= P ∨ ¬P

_{を 用いて ，}

⊥, ⊤

を 消す．

(Step 2) A ↔ B ∼= (A → B) ∧ (B → A)

を 用いて

↔

を 消 す．

(Step 3) A → B ∼= ¬A ∨ B

_{を 用いて}

→

を 消す．

(Step 4) ¬(A ∧ B) ∼= ¬A ∨ ¬B

_，

¬(A ∨ B) ∼= ¬A ∧ ¬B

_を 用いて ，

¬

が，

∧

や

∨

の外側には出現し ないよ う にする ．

(Step 5) ¬¬A ∼= A

を 用いて ， 命題変数の外には

¬

が

1

つ以 下し か出現し ないよ う にする ．

[

論理積標準形の場合

]

(Step 6) (A∧B)∨C ∼= (A∨C)∧(B∨C)

およ び

C∨(A∧B) ∼= (C ∨ A) ∧ (C ∨ B)

を 用いて ，

∨

の内側に

∧

が出現し ないよ

う にする ．

[

論理和標準形の場合

]

(Step 6) (A∨B)∧C ∼= (A∧C)∨(B∧C)

およ び

C∧(A∨B) ∼= (C ∧ A) ∨ (C ∧ B)

を 用いて ，

∧

の内側に

∨

が出現し ないよ

う にする ．

注意 ： 論理式の形が適切な論理的同値式なら ば論理積

(

論理 和

)

標準形なので， 一般に命題論理式

A

_の論理積

(

論理和

)

標 準形は

1

つと は限ら ない． ま た， 上の計算の通り にやら ない で他の同値変形を 用いて 変形し て も よ い．

例えば，

P∧Q

は論理積

(

論理和

)

標準形だが，

Q∧P

も

P∧Q

の論理積

(

論理和

)

標準形．

命題論理式の標準形

定義

4.11.

命題論理式

A

と 論理的同値な 論理積標準形

を 命題論理式

A

の論理積標準形と よ ぶ． 命題論理式

A

_{と 論} 理的同値な論理和標準形を 命題論理式

A

_{の論理和標準形と} よ ぶ．

演習

4.12.

次の命題論理式の論理積標準形と 論理和標準

形を 求めよ ．

(1) ¬¬P → Q

(2) (P → Q) → R → S

(1) ¬¬P → Q

∼= ¬¬¬P ∨ Q (

含意

)

∼= ¬P ∨ Q (

二重否定

) · · ·

論理和標準形， 論理積標準形

(2) (P → Q) → (R → S)

∼= (P → Q) → (¬R ∨ S) (

含意

)

∼= (¬P ∨ Q) → (¬R ∨ S) (

含意

)

∼= ¬(¬P ∨ Q) ∨ (¬R ∨ S) (

含意

)

∼= (¬¬P ∧ ¬Q) ∨ (¬R ∨ S) (

ド ・ モルガン

)

∼= (P ∧ ¬Q) ∨ ¬R ∨ S (

二重否定

) · · ·

論理和標準形

∼= (P ∨ ¬R ∨ S) ∧ (¬Q ∨ ¬R ∨ S) (

分配律

) · · ·

論理積標準形

真理値表から の標準形の構成

すでに与えら れた命題論理式を 標準形に変換する 方法を

紹介し た． こ こ では， 標準形を 得る 別の方法と し て， 標準形

を そ の命題論理式の真理値表から 構成する 方法を 紹介する ．

論理和標準形の構成法

¬(P → Q ∧ R)

を 例にと っ て 説明する ．

(1)

ま ず， 真理値表を 作る ．

P Q R · · · ¬(P → (Q ∧ R))

T T T · · · F

T T F · · · T

T F T · · · T

T F F · · · F

F T T · · · T

F T F · · · F

F F T · · · F

F F F · · · F

P Q R · · · ¬(P → (Q ∧ R))

T T T · · · F

T T F · · · T

T F T · · · T

T F F · · · F

F T T · · · T

F T F · · · F

F F T · · · F

F F F · · · F

(2)

こ のと き ，

¬(P → Q∧ R)

が真と なる のは

3

通り ． そ のそ

れぞれの場合について ， 真なら そ の命題変数， 偽なら そ の

命題変数の否定を と っ たリ テラ ルの論理積を 考える ．

P Q R · · · ¬(P → (Q ∧ R))

T T T · · · F

T T F · · · T

T F T · · · T

T F F · · · F

F T T · · · T

F T F · · · F

F F T · · · F

F F F · · · F

(2)

こ のと き ，

¬(P → Q∧ R)

が真と なる のは

3

通り ． そ のそ れぞれの場合について ， 真なら そ の命題変数， 偽なら そ の 命題変数の否定を と っ たリ テラ ルの論理積を 考える ．

P ∧ Q ∧ ¬R

P Q R · · · ¬(P → (Q ∧ R))

T T T · · · F

T T F · · · T

T F T · · · T

T F F · · · F

F T T · · · T

F T F · · · F

F F T · · · F

F F F · · · F

(3)

得ら れた論理積の論理和を と る ．

(P ∧ Q ∧ ¬R) ∨ (P ∧ ¬Q ∧ R) ∨ (¬P ∧ Q ∧ R)

こ の命題論理式は

W

i

V

j L_ij

の形になっ て おり ， ま た， 同じ

真理値表を も つので， 元の命題論理式と 論理的同値． 従っ

て 論理和標準形．

演習

4.13.

次の命題論理式の論理和標準形を 真理値表か ら 求めよ ．

(1) P ∨ Q → P ∧ Q (2) ¬(P → Q) ∨ P

P Q P ∨ Q P ∧ Q (P ∨ Q) → (P ∧ Q)

T T T T T

T F T F F

F T T F F

F F F F T

P Q P → Q ¬(P → Q) (¬(P → Q)) ∨ P

T T T F T

T F F T T

F T T F F

F F T F F

(

解答

) (1)

P Q P ∨ Q P ∧ Q (P ∨ Q) → (P ∧ Q)

T T T T T

T F T F F

F T T F F

F F F F T

赤字の行に着目する と ， 論理和標準形

(P∧Q) ∨ (¬P∧ ¬Q)

が 得ら れる ．

(2)

紹介し た手続き に従う と ， 論理和標準形

(P∧Q)∨(P∧¬Q)

が得ら れる

(

が， 真理値表から ，

P ∼= (¬(P → Q)) ∨ P

が確認

でき る から ， も っ と 簡単に， 論理和標準形と し て

P

_{を と っ て}

も よ い．

)

論理積標準形の構成法

(P → Q) → Q ∧ ¬P

を 例にし て 説明する ．

(1)

ま ず， 真理値表を 構成する ． 真理値表は

P Q · · · (P → Q) → (Q ∧ (¬P))

T T · · · F

T F · · · T

F T · · · T

F F · · · F

と なる ．

(2)

論理和標準形のと き は， 与式が真と なる 行に着目し た．

論理積標準形の場合は与式が偽と なる 行に着目する ． 与式

が偽と なる のは，

P∧Q

が真の場合

(1

行目

)

， ま たは，

¬P∧¬Q

が真の場合

(4

行目

)

である ．

P Q · · · (P → Q) → (Q ∧ (¬P))

T T · · · F

T F · · · T

F T · · · T

F F · · · F

(3)

従っ て ， 与式が真と なる のは， こ れら のど ち ら でも な い場合， つま り ，

¬(P ∧ Q) ∧ ¬(¬P ∧ ¬Q)

と なる 場合である ． こ れを ド ・ モルガン の法則と 二重否定 の法則で同値変形する と ， 次の論理積標準形が得ら れる ．

(¬P ∨ ¬Q) ∧ (P ∨ Q)

演習

4.14.

次の命題論理式の論理積標準形を 真理値表か ら 求めよ ．

(1) P ∨ Q → P ∧ Q

(2) ¬((¬P → Q) → P)

P Q P ∨ Q P ∧ Q (P ∨ Q) → (P ∧ Q)

T T T T T

T F T F F

F T T F F

F F F F T

P Q ¬P ¬P → Q ((¬P) → Q) → P ¬(((¬P) → Q) → P)

T T F T T F

T F F T T F

F T T T F T

F F T F T F

(

解答

) (1)

P Q P ∨ Q P ∧ Q (P ∨ Q) → (P ∧ Q)

T T T T T

T F T F F

F T T F F

F F F F T

赤字の行に着目する と ，

(¬((P ∧ ¬Q) ∨ (¬P ∧ Q))

から

)

論理 積標準形

(¬P ∨ Q) ∧ (P ∨ ¬Q)

が得ら れる ．

(2)

紹介し た手続き に従う と ， 論理積標準形

(¬P ∨ ¬Q) ∧ (¬P ∨ Q) ∧ (P ∨ Q)

が得ら れる

(

が， こ の場合は，

T

と なる 行

が

1

つし かないので， 論理和標準形の構成法で， 論理積標準

形かつ論理和標準形である

¬P ∧ Q

_{が得ら れる}

)

．

ま と め

•

命題論理式の同値変形 論理的同値性

重要な同値式

•

論理積標準形

(CNF)

， 論理和標準形

(DNF)

同値変形によ る 標準形への変換

真理値表にも と づく 標準形の構成法

補足資料

以下は， 特に興味のある 人へ， 関連する 発展的な話題の 紹介． 講義では取り 上げま せん．

         

目次 ( 補足資料 )

-

命題論理式の表現力と 命題結合子の完全性

- CNF

への充足可能性保存変換

- SAT

ソ ルバを 用いた問題解決

命題論理式の表現力

n

引数ブール関数に対応する 命題変数

{P₁, . . . , P_n}

上の命 題論理式

A

は， 真理値表に基づく 論理和

(

積

)

標準形構成法 で構成でき る ．

(1) 2

引数ブール関数を

f

と する と ， 対応する 真理値表は 以下のよ う になっ て いる はず．

P₁ P₂ · · · A

T T · · · f(T,T)

T F · · · f(T,F)

F T · · · f(F,T)

F F · · · f(F,F)

真理値表から の論理和

(

積

)

標準形の構成には，

P₁, . . . , P_n

の真理値と ， 命題論理式全体の真理値の対応で充分．

(2)

構成さ れた論理和

(

積

)

標準形

A

は， 同じ 真理値表を 持つ． 従っ て ，

P₁ P₂ · · · A

T T · · · f(T,T)

T F · · · f(T,F)

F T · · · f(F,T)

F F · · · f(F,F)

つま り ， 任意の付値

v

_{について ，}

f(v(P₁), . . . , v(P_n)) = [[A]]_v

．

以上の議論によ り ，

定理

4.15. f

_{を 任意の}

n

引数ブール関数と する ． こ のと き ，

f(v(P₁), . . . , v(P_n)) = [[A]]_v

が任意の付値

v

_{について 成立す}

る よ う な命題論理式

A

_{が存在する ．}

命題結合子の完全性

標準形は，

∧, ∨, ¬

し か用いて いない． 従っ て ， 以下の定 理が成立する ．

定理

4.16.

任意の命題論理式

A

_{に対し て，}

∨, ∧, ¬

のみを 命 題結合子に用いた命題論理式

B

_で，

A ∼= B

_{と なる も のが存} 在する ．

更に， 論理的同値式

A ∧ B ∼= ¬((¬A) ∨ (¬B))

を 用いて 変形する こ と が出来る ので， 次の結果も 成立する ．

定理

4.17.

任意の命題論理式

A

_{に対し て，}

∨, ¬

のみを 命題

結合子に用いた命題論理式

B

_で，

A ∼= B

と なる も のが存在

する ．

前ページの定理が成立する こ と を「

{∨, ¬}

が完全である 」 と いう ．

{∨, ¬}

の他に，

{∧, ¬}

も 完全． 一方，

{¬}

や

{∧, ∨}

は完 全ではない．

演習

4.18. ∧, ∨

だけ し か用いて いないど の命題論理式と

も 同値と はなら ない命題論理式を 与え ， そ う なる 理由を 示

せ．

さ ま ざま な命題結合子

今ま で出て き た命題結合子

¬, ∧, ∨, →, ↔, ⊥, ⊤

と は異な る 命題結合子が使われる こ と がある ． し かし ながら ， 完全 性から 少なく て も

¬, ∧

等があればど のよ う な命題結合子で あろ う と ， そ れら を 等価な命題論理式の省略形と 考え て よ い こ と がわかる ．

はいたて き

排他的論理和

(exclusive or)

， 記号

: ⊕, +

など ．

A B A ⊕ B T T F T F T F T T F F F

A ⊕ B ∼= (A ∨ B) ∧ ¬(A ∧ B)

否定的論理積

(negative and, NAND)

， 記号

: |

など ．

A B A | B T T F T F T F T T F F T

A | B ∼= ¬(A ∧ B)

否定的論理和

(negative or, NOR)

， 記号

: k, ↓

など ．

A B A k B T T F T F F F T F F F T

A k B ∼= ¬(A ∨ B)

{⊕, ¬}

は完全ではない． 一方，

{ | }

およ び

{ k }

は完全に なる ．

演習

4.19. { | }

およ び

{ k }

が完全である こ と を 示せ．

演習

4.20.

与えう る

2

引数結合子

c

_{のう ちで，}

{c}

が完全に

なる のは，

|

およ び

k

のみである ． こ のこ と を 示せ．

目次 ( 補足資料 )

-

命題論理式の表現力と 命題結合子の完全性

- CNF

への充足可能性保存変換

- SAT

ソ ルバを 用いた問題解決

標準形への変換の効率性

論理積標準形

(CNF)

に対する 効率的な充足可能性判定シ ステム

(SAT

ソ ルバ

)

が開発さ れて いる ． し かし ながら ， 論 理的同値性に基づく 論理積標準形への変換や真理値表の構 成を 経由し た論理積標準形への変換は， 計算時間の観点か ら ， 実際的でない．

し かし ， 充足可能性を 保存する

CNF

への効率的な変換

(

充足可能性保存変換

)

が知ら れて おり ，

SAT

ソ ルバで充足

可能性を 判定する 場合は， こ ち ら を 用いる ．

(

こ の変換は論

理的同値性は保存し ない．

)

論理積標準形への充足可能性保存変換

ア イ デア ： 部分式を 新し い命題変数に対応さ せる ． 例．

((P ∧ Q) ∨ R)

の変換

(P ∧ Q) ∨ R (P ∧ Q)

を 命題変数

N

_{と おく}

❀ (N ∨ R) ∧ (N → (P ∧ Q)) ∧ ((P ∧ Q) → N)

❀ (N ∨ R) ∧ ((¬N) ∨ (P ∧ Q)) ∧ ((P ∧ Q) → N)

❀ (N ∨ R) ∧ ((¬N) ∨ P) ∧ ((¬N) ∨ Q) ∧ ((P ∧ Q) → N)

❀ (N ∨ R) ∧ ((¬N) ∨ P) ∧ ((¬N) ∨ Q) ∧ (¬(P ∧ Q) ∨ N)

❀ (N ∨ R) ∧ ((¬N) ∨ P) ∧ ((¬N) ∨ Q) ∧ ((¬P) ∨ (¬Q) ∨ N)

つま り ， 部分式

P ∧ Q

を

N

と 置き 換える と と も に，

(P ∧ Q)

と

N

の同値性を 示す式

(

あら かじ め， こ の式自体も

CNF

にし

て おく

)

を 追加する ．

以下で，

{P 7→ B}(A)

は

A

_{中の命題変数}

P

_{を すべて}

B

_に 置き 替える 操作を 表わす．

定理

4.21. A, B

_{を命題論理式，}

P

_{を命題論理式}

B

_に出現し ない命題変数と する ． こ のと き ，

{P 7→ B}(A)

が充足可能

⇔ A ∧ (P ↔ B)

が充足可能．

(

証明

) (⇒) {P 7→ B}(A)

が充足可能と する ． こ のと き ，

[[{P 7→ B}(A)]]_v = T

なる 付値

v

が存在する ． こ のと き ，

v^′(P) = [[B]]_v

，

P 6= Q

_{なる 全て の}

Q

_について

v^′(Q) = v(Q)

なる 付値

v^′

_{を 考え る ．}

P

_が

B

に出現し ないこ と から ，

[[P ]]_v^′ = v^′(P) = [[B]]_v = [[B]]_v^′

が成立す る ． よ っ て ，

[[A]]_v^′ = T

と なる ． よ っ て ，

A ∧ (P ↔ B)

も 充足可能．

(⇐) [[A ∧ (P ↔ B)]]_v = T

と する と

[[P]]_v = [[B]]_v

である から ，

[[{P 7→ B}(A)]]_v = [[A]]_v

． よ っ て ，

{P 7→ B}(A)

も 充足

可能．

変換テーブル

N ↔ ⊥ ⇔ (N → ⊥) ∧ (⊥ → N)

⇔ ¬N

N ↔ ⊤ ⇔ (N → ⊤) ∧ (⊤ → N)

⇔ N

N ↔ (¬P) ⇔ (N → ¬P) ∧ (¬P → N)

⇔ (¬N ∨ ¬P) ∧ (P ∨ N)

N ↔ (P ∧ Q) ⇔ (N → (P ∧ Q)) ∧ ((P ∧ Q) → N)

⇔ ((¬N) ∨ (P ∧ Q)) ∧ (¬(P ∧ Q) ∨ N)

⇔ (((¬N) ∨ P) ∧ ((¬N) ∨ Q)) ∧ ((¬P) ∨ (¬Q) ∨ N) N ↔ (P ∨ Q) ⇔ (N → (P ∨ Q)) ∧ ((P ∨ Q) → N)

⇔ ((¬N) ∨ (P ∨ Q)) ∧ (¬(P ∨ Q) ∨ N)

⇔ ((¬N) ∨ P ∨ Q) ∧ (((¬P) ∧ (¬Q)) ∨ N)

⇔ ((¬N) ∨ P ∨ Q) ∧ ((¬P) ∨ N) ∧ ((¬Q) ∨ N) N ↔ (P → Q) ⇔ · · ·

N ↔ (P ↔ Q) ⇔ · · ·

例．

(P₁ ∧ P₂) ∨ (¬(P₃ ∨ P₄))

の変換

(P₁ ∧ P₂)

6 ∨ (¬(P₃ ∨ P₄)

8)

75

❀ P₅ ∧ (P₅ ↔ (P₆ ∨ P₇))

∧ (P₆ ↔ (P₁ ∧ P₂))

∧ (P₇ ↔ (¬P₈))

∧ (P₈ ↔ (P₃ ∨ P₄))

❀ P₅ ∧ ((¬P₅) ∨ P₆ ∨ P₇) ∧ ((¬P₆) ∨ P₅) ∧ ((¬P₇) ∨ P₅)

∧ (P₆ ∨ (¬P₁) ∨ (¬P₂)) ∧ ((¬P₆) ∨ P₁) ∧ ((¬P₆) ∨ P₂)

∧ ((¬P₇) ∨ (¬P₈)) ∧ (P₇ ∨ P₈)

∧ ((¬P₈) ∨ P₃ ∨ P₄) ∧ ((¬P₃) ∨ P₈) ∧ ((¬P₄) ∨ P₈)

演習

4.22.

充足可能性保存変換が論理的同値性を 保存し

ないのはなぜか， 考えよ ．

目次 ( 補足資料 )

-

命題論理式の表現力と 命題結合子の完全性

- CNF

への充足可能性保存変換

- SAT

ソ ルバを 用いた問題解決

SAT ソ ルバ

命題論理式が与えら れたと き に， そ れが充足可能かど う かを 答え よ ， と いう 問題を 充足可能性

(SAT)

問題と いう ． 充足可能性問題は，

NP

完全問題． 従っ て ， 効率的に解く の は困難．

SAT

問題を

(

高速に

)

解く ソ フ ト ウ ェ ア が研究・ 開発さ れ て いる ． こ れら は

SAT

ソ ルバと よ ばれる ．

(NP

完全問題な ので効率的には解けないが， 人の問題を 扱う 論理式の充足 可能性は高速に判定でき る こ と がよ く ある ．

)

ある 種の問題は，

SAT

問題に帰着さ せる こ と で，

SAT

ソ

ルバを 用いて 解く こ と が出来る ．

SAT

ソ ルバを 用いた問題

解決の例を 学習する ．

SAT ソ ルバの使用例

(P₁ ∨ P₃ ∨ ¬P₄) ∧ P₄ ∧ (P₂ ∨ ¬P₃)

の充足可能性を 判定し て みる ．

%cat sample <---

入力フ ァ イ ルの表示

p cnf 4 3

1 3 -4 0 4 0

2 -3 0

%./minisat sample out <--- minisat

の実行

....

....

SATISFIABLE

%cat out <---

出力フ ァ イ ルの表示

SAT

-1 2 3 4 0

DPLL ア ルゴリ ズム

多く の

SAT

ソ ルバで用いら れて いる ア ルゴリ ズム

(

以下は 非常に単純化し たバージョ ン

)

fun isSatisfiable

節集合

S =

while

単位節

{L} ∈ S do (* unit propagation *) L

を 含む節を

S

から 消去

S

中の，

L

を 含む節から

L

を 消去

if S = ∅ then True

else if ∅ ∈ S then False

リ テラ ル

L

_を

S

_から

1

つ選ぶ

(* splitting *) if isSatisfiable S ∪ {{L}} then True

else if isSatisfiable S ∪ {{L}} then True else False

(

参考

) DPLL

ア ルゴリ ズムや

SAT

ソ ルバについて よ り 詳し く 知り たい人には， 以下を 見る と よ い．

• John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009.

定理自動証明の話題を 広く 網羅し た数理論理学の教科書

• Filip Mari´c, Formalization and Implementation of Modern SAT Solvers, Journal of Automated Reasoning, Vol. 43, pp. 81–119, 2009.

近年のテク ニッ ク にも と づく

SAT

ソ ルバの原理につい

て の解説論文．

SAT ソ ルバを 使っ た問題解決の例 : n _{ク イ ーン 問題}

n

_{ク イ ーン 問題：}

n

×

n

のマス上を

Queen

は縦， 横， 斜めに動く ． こ のと き ，

Queen

同士が取り 合わないよ う に，

n

_個の

Queen

が置 く こ と が出来る か？

Q Q

Q Q

Q

n ク イ ーン 問題の符号化 (1)

各マスのそ れぞれに命題変数を

1

つ割り 当て る ．

P₁₁ P₁₂ · · · P_1n

P₂₁ P₂₂ · · · P_2n . . . . P_n1 P_n2 · · · P_nn

v(P_ij) = T ⇐⇒ Queen

が第

(i, j)

マス乗っ て いる

v(P_ij) = F ⇐⇒ Queen

が第

(i, j)

マス乗っ て いない

と 解釈し て ，

n

_{ク イ ーン 問題を}

SAT

問題に符号化する ．

n ク イ ーン 問題の符号化 (2)

(A)

各行について ， 同時に

2

箇所に置かれる こ と はない

^

i

^

j₁6=j₂

¬(P_ij1 ∧ P_ij2)

(B)

各列について ， 同時に

2

箇所に置かれる こ と はない

^

j

^

i₁6=i₂

¬(P_i1j ∧ P_i2j)

(C)

各斜めについて ， 同時に

2

箇所に置かれる こ と はない





_

i^′−i=j^′−j

¬(P_ij ∧ P_i^′_j^′)



 ∧





_

i^′−i=j−j^′

¬(P_ij ∧ P_i^′_j^′)





(D)

各行について ，

1

箇所には置かれて いる

^

i

_

j

P_ij

n

個のク イ ーン が置ける

⇐⇒

命題論理式

(A) ∧ (B) ∧ (C) ∧ (D)

が充足可能

プログラ ム例

(*

命題変数

*) val nvars = ref 0

fun fresh () = (nvars := (!nvars) + 1; !nvars) (* CNF

への充足可能性保存変換

*)

val cnf = ref [] : int list list ref fun conj xs =

let val y = fresh () in

((cnf p:= (y :: map (fn x => ~x) xs)

:: (map (fn x => [~y, x]) xs) @ (!cnf));

y) end

...

(* n

ク イ ーン 問題の制約

*)

fun pvar col (i,j) = i * col + j + 1

(* col * col

以下はそれぞれのマ スに対応する 命題変数

*)

fun constraintExist col =

let fun constraintLine i =

disj (List.tabulate (col, fn j => pvar col (i,j))) in

conj (List.tabulate (col, fn i => constraintLine i)) end

...

fun nQueenConstraint col = let

val z = conj [ constraintExist col, constraintTate col, ....

] in

[z] :: !cnf end

fun nQueen col =

(nvars := col * col; cnf := [];

nQueenConstraint col)

テスト 例

%sml @SMLload=nqueen.x86-bsd 5 > 5.cnf <---

作成プロ グラ ム で

CNF

を フ ァ イ ルに出力

%cat 5.cnf

p cnf 690 1733 690 0

690 -31 -187 -343 -439 -504 -600 -689 0 -690 31 0

-690 187 0 -690 343 0 ....

%./minisat 5.cnf 5.out <--- SAT

ソ ルバ実行

....

SATISFIABLE

%cat 5.out SAT

-1 -2 -3 -4 5 -6 -7 8 -9 -10 11 -12 -13 -14 -15 -16 -17 -18 19 -20 -21 22 -23 -24 -25 26 27 28 29 30 31 32 -33 34 -35 -36 37 -38 39 -40 41 42 43 44 45 46 47 48 49 50 -51 52 53 54 55 56 57 58 59 60 61 62 63 -64 65 -66 67 -68 69 -70 -71 ....

先頭の方の付値を 見る こ と で解がわかる ．

Q Q

Q Q

Q