前束范式流水线Prenex · Skolem

谓词公式的前束范式（PNF）半自动变换器。选一个公式，点「下一步」逐阶段推导：消去 → ↔ → 否定内移(NNF) → 约束变元改名 → 量词前移(PNF) → Skolem 化。每步高亮改动并注明所用规则。

选择预置公式

当前公式 φ

步骤 1–4 保持逻辑等值（≡）；Skolem 化只保持可满足性（等可满足）而非等值 —— 引入 Skolem 常元/函数替换存在量词。
存在量词前无 ∀ ⟹ Skolem 常元；前有 ∀ ⟹ Skolem 函数（以那些全称变元为参数）。