節集合(set of clause)への変換

節 (clause)


[定義] 節 (clause) リテラルの選言を 節という．表記上，節はリテラルの集合として表現する．

(例) 例えば，P ∨ Q ∨ ¬R ⇒ {P, Q, ¬R}

r個のリテラルからなる節をrリテラル節 と呼ぶ．

一個のリテラルからなる節を単一節(unit clause) とよび，リテラルを含まない節を空節 (empty clause) とよぶ．

節の集合 S は S に含まれる全ての節の連言であり，S の全ての自由変 数は全称限量記号により束縛されていると約束することで，Skolem標準形を節 の集合 (節集合: set of clauses)とよぶ．

(例)
(∀x)(∃y)(∃z)((¬P(x, y) ∧ Q(x, z)) ∨ R(x, y, z)) の Skolem標準形 は
(∀x)((¬P(x, f(x)) ∨ R(x, f(x), g(x))) ∧ (Q(x, g(x)) ∨ R(x, f(x), g(x))) )．
節集合としての表記は{{¬P(x, f(x)), R(x, f(x), g(x))}, {Q(x, g(x)), R(x, f(x), g(x))}}

節集合の充足不能性


[定理] 節の充足不能性 S を 式 F の 標準形をあらわす節集合とする．F が充足不能であるための必要十分条件は， S が充足不能 (演繹導出として反駁が得られる)であることである．

...Return

• 講義の詳細