融合節の生成 (Resolution and Resolvent)

融合節 (resolvent)

[定義] 因子 (factor) 節 C の2個以上の同一符号のリテラルの集合が最汎単一子 σ を持つとき， Cσ を C の因子 (factor)と呼ぶ．特に Cσが単一節のとき，それを C の単一因子 (unit factor)とよぶ．

[定義] 二項融合節 (binary resolvent) C₁ と C₂ を共通変数を持たない節とし， L₁, L₂(ただしL₁ ≠ L₂) をそれぞれC₁，C₂ のリテラルとする．L₁， ¬L₂ が最汎単一子 σ を持つとき，節

(C₁σ - L₁σ) ∪(C₂σ - L₂σ)

をC₁ と C₂ の二項融合節 (binary resolvent)と呼ぶ．またそのとき，C₁ と C₂ を親節(parent clause)， L₁, L₂ を融合リテラル (literals resolved upon) という．

(例)
C₁ = {P(x), Q(x)}, C₂ = {¬P(a), R(y)}の二項融合節を求めよ．

[定義] 融合節 (resolvent) 次のものを節 C₁ と C₂ の融合節 (resolvent) という．

(例)
1. C₁ = {P(x), P(f(y)), R(g(y))} と C₂ = {¬ P(f(g(a))), Q(b)} との融合節を求めよ．

2. C₁ = {P(f(y)), Q(g(x))} と C₂ = {¬ P(f(g(a))), Q(f(a))} の融合節を求めよ．