スコーレム標準形(Skolem Normal Form)への変換

目的


論理式中に現れる論理変数を可能な限り定項と関数記号を用いて表現す ることで，具体的な解釈を定め，それによりモデル解釈を可能にするため．

(例) ∀x∃yP(x,y) という論理式を考える．

(例) ∀x∀y∃z(P(x,y)→Q(z))という論理式 を考える．

スコーレム標準形(スコーレム化)


[定義] スコーレム標準形 式 F = (Q₁x₁)...(Q_nx_n)αの Skolem標準形は冠頭標準形から次のようにして構成される．論理式をSkolem標 準形に変換することをスコーレム化 (skolemization)と呼ぶ．

1. αを冠頭連言標準形に変換する．

2. Q_r (1 ≦r ≦n) を冠頭部: (Q₁x₁)...(Q_nx_n) における存 在限量記号とする．Q_s1x_s1, ..., Q_smx_sm (1 ≦ x_s1 ＜x_s2 ＜・・・＜ x_sm ＜r)を Q_r　の前に現れる全ての全称 限量記号とすると，他のどの関数記号とも異なる新しい m-引数関数記号 f を 選び，αにおける x_r の全ての出現を f(x_s1, x_s2, ・・・, x_sm)　で置き換え，冠頭部から　 (Q_rx_r)を取り除く．
   特殊な場合として，冠頭部の Q_r の前に全称限量記号が現れてい ないときは，αの他のどの定数記号とも異なる新しい定数 c を導入して，α における x_r の全ての出現を c で置き換え，冠頭部から (Q_rx_r)を取り除く．

(例) 以下の論理式をスコーレム化せよ．
1. (∀x)(∀y)(∃z)(P(x, y) → Q(z))

2. (∀x₁)(∃y₁)(∀x₂)(∃y₂)(P(x₁, y₁)∧Q(x₂, y₂) → R(x₁,y₂))

...Return

• 講義の詳細