Module 04

反駁手続きと自動定理証明

背理法に基づく反駁手続き（resolution refutation）を体験する。 「結論の否定 → 標準形 → 空節 □\square の導出」というフローで論理的帰結を機械的に証明する。

基本原理（定理 2.1 / 2.2 / 4.1）

「Γ⊨φ\Gamma \models \varphi ⟺ Γ∪{¬φ}\Gamma \cup \{\lnot \varphi\} は矛盾する」 という同値性により、論理的帰結の証明は 否定の矛盾性 を示す問題に帰着できる。

さらに定理 4.1 により、節集合のスコーレム化は矛盾性を保つので、 一階論理の論理的帰結であっても、節集合に対するレゾリューション規則の適用だけで機械的に判定できる。

C∨LD∨¬LC∨D(Resolution Rule)\dfrac{C \lor L \quad D \lor \lnot L}{C \lor D} \quad (\text{Resolution Rule})

証明シミュレーター

課題を選び、3 段階のフローを順番に進める。最後に空節 □\square を導けば反駁完了。

課題
次の論理的帰結を反駁手続きで証明する：
P→Q,  P  ⊨  QP \to Q,\; P \;\models\; Q
1

結論を否定する

背理法のため、結論 QQ の否定を仮定し、 前提と合わせて矛盾を導く。

¬(Q)\lnot \left(Q\right)
2

標準形（節集合）にする

前提と ¬\lnot 結論をすべて CNF に変形し、節（ ∨\lor の連なり）の集合として扱う。

  1. 前提 1
    P→Q  ⇒  ¬P∨QP \to Q \;\Rightarrow\; \lnot P \lor Q
  2. 前提 2
    P  ⇒  PP \;\Rightarrow\; P
  3. 結論の否定
    ¬Q  ⇒  ¬Q\lnot Q \;\Rightarrow\; \lnot Q
3

レゾリューションで空節 □ を導く

2 つの節を選択し「レゾリューション」を押すと、相補リテラル（ LL と ¬L\lnot L ）が消去された新しい節が生成される。 空節 □\square を導けば反駁完了。