冠頭標準形(Prenex Normarl Form)への変換

目的

論理式を節集合に変換することで，融合原理を適用できるようにするため．

閉形 (closure)

論理式 F に含まれている自由変数を x₁, x₂, ・・・, x_nとするとき，

(∀x₁)(∀x₂)・・・(∀x_n)F を全称閉形 (universal closure)
(∃x₁)(∃x₂)・・・(∃x_n)F を存在閉形 (existential closure)

という．

(演習問題) P(x) → (∃x)P(x)の全称閉形は?

(1) ある論理式が恒真かどうか調べるためにはその論理式に現れる自由変数について全称閉形をとった論理式を作った後に，その恒真性を調べればよい．

(2)ある論理式が恒偽かどうか調べるためにはその論理式の存在閉形をとった論理式を作った後に，その充足不能性を調べればよい．

冠頭標準形(prenex normal form)

任意の論理式は次のような形式に変換することが可能(以下の Q は全称限量子か存在限量子のいずれか)

[冠頭連言標準形 (prenex-conjunctive normal form)]

(Qx₁)(Qx₂)・・・(Qx_n){(A₁₁ ∨ ・・・ ∨ A_1k₁) ∧
　　　　　　　　　　　　(A₂₁ ∨ ・・・ ∨ A_2k₂)∧
　　　　　　　　　　　　　　　・・・・・・
　　　　　　　　　　　　(A_j1 ∨ ・・・ ∨ A_{jk_j})}

[冠頭選言標準形 (prenex-disjunctive normal form)]

(Qx₁)(Qx₂)・・・(Qx_n){(A₁₁ ∧ ・・・ ∧ A_1k₁) ∨
　　　　　　　　　　　　(A₂₁ ∧ ・・・ ∧ A_2k₂)∨
　　　　　　　　　　　　　　　・・・・・・
　　　　　　　　　　　　(A_j1 ∧ ・・・ ∧ A_{jk_j})}

ただし，A₁₁，・・・, A_{jk_j} はすべてリテラルで，各素論理式に現れる全ての変数は x₁, x₂, ・・・x_nとして式の左端(冠頭)に取り出されていることとする．

(Qx₁)(Qx₂)・・・(Qx_n)を冠頭部 (prefix)，それより右の { } の部分を本体 (matrix)という．

標準形変換アルゴリズムII

[ステップ1] 限量子 (Qx) の作用域に x が現れない場合，その限量子を除去する．(e.g. (∀x(P(y) → Q(z)) = (P(y) → Q(z)))

[ステップ2] ∧，∨，¬ 以外の論理演算子は，同値の式を用いてすべて除去する．

[ステップ3] ¬ を一番内側にうつす．そのときに以下の規則を適用する．

¬¬α = α
¬ (α ∨ β) = ¬α ∧ ¬β
¬ (α ∧ β) = ¬α ∨ ¬β
¬ ((∀x)α) = (∃x)(¬α)
¬ ((∃x)α) = (∀x)¬(α)

[ステップ4] 必要であれば束縛変数のつけかえを行う(ステップ5を参照)．

すなわち (∀x)A(x)，(∃x)A(x) の形をした部分論理式における束縛変数 x が論理式中の他の変数と同じであれば，全て異なるようにつけかえる．これは，式のもっとも左側に現れる束縛変数から順に新しい変数におきかえていく．

[ステップ5] 限量子を本体の左に動かす．そのときに以下の規則を適用する．ただし，式中の G は変数 x を含まないものとする．

(∀x)F(x) ∧ G = (∀x)(F(x) ∧ G)
(∀x)F(x) ∨ G = (∀x)(F(x) ∨ G)
(∃x)F(x) ∧ G = (∃x)(F(x) ∧ G)
(∃x)F(x) ∨ G = (∃x)(F(x) ∨ G)

以下に注意すること．

(∀x)F(x) ∧ (∀x)G(x) = (∀x)(F(x) ∧ G(x))
(∃x)F(x) ∨ (∃x)G(x) = (∃x)(F(x) ∨ G(x))
(∀x)F(x) ∨ (∀x)G(x) = (∀x)(∀y)(F(x) ∨ G(y))
　　　　　　　　　　　　　　≠ (∀x)(F(x) ∨ G(x))
(∃x)F(x) ∧ (∃x)G(x) = (∃x)(∃y)(F(x) ∧ G(y))
　　　　　　　　　　　　　　≠ (∃x)(F(x) ∧ G(x))

(Q₁x)F(x) ∨ (Q₂x)G(x) = (Q₁x)(Q₂y)(F(x) ∨ G(y))
(Q₁x)F(x) ∧ (Q₂x)G(x) = (Q₁x)(Q₂y)(F(x) ∧ G(y))

[ステップ6] 次の分配則を用いて，連言標準形，選言標準形を作る．

F ∨ (G ∧ H) = (F ∨ G) ∧ (F ∨ H)
F ∧ (G ∨ H) = (F ∧ G) ∨ (F ∧ H)

さらに，これらの式の変形ステップの途中で同値な式の規則を適宜使用することができる．

(演習問題)

以下の論理式を冠頭連言標準形に変換せよ．

(∀x)P(x) → (∃x)Q(x)

(∀x)(∀y)[(∃z)(P(x, z) ∧ P(y, z)) → (∃u)Q(x, y, u)]

...Return

講義の詳細