節集合と空節
配列構造に変換する
開発者向け解説
スコーレム化が終わると、式の中の変数はすべて ∀ で縛られていることが確定します。 そこで、コンピュータが配列として処理しやすくするために、 論理式から不要な記号（∀ や ∧）をすべて削ぎ落とし、リテラル（P や ¬Q）が ∨ で繋がったグループ（節）のリスト（節集合）に変換します。
最も重要なのが 空節（empty clause, □）です。これはリテラルを1つも含まない節[]であり、何をどうしても真にできない「究極の矛盾」を表します。この □ を導き出すことが、自動定理証明のゴールです。
下のクリーナーで、∀ と ∧ が消えて配列になる過程を 4 ステージで体験してください。
プリセット式（スコーレム化済み）
変形ステージ
- Stage 0：もとの式
スコーレム化が終わると、変数はすべて ∀ で縛られています。
∀x ((¬P(x) ∨ Q(x)) ∧ R(f(a)))
空節 □
リテラルが 1 つも含まれない節（空のリスト []）が空節 □ です。 これは何をどうしても真にできない「究極の矛盾」を表します。 反駁手続きが □ を導き出した瞬間、 「もとの式の否定が矛盾する＝もとの式は妥当（valid）」と判定されます。これが自動定理証明のゴールです。