前束范式（Prenex Normal Form，PNF）：一种形式逻辑中的标准化写法，把所有量词（如 ∀“对所有”、∃“存在”）都移动到公式最前面，形成“量词前缀 + 无量词的矩阵（matrix）”的结构，同时保持（在适当变形下）与原公式等价或可满足性等价。常用于一阶逻辑的证明、自动推理与规范化转换。（注：不同教材中对“保持等价”与“保持可满足性”的要求可能略有差异，尤其与 Skolem 化相关。）
/ˈpriːnɛks ˈnɔːrməl fɔːrm/
A prenex normal form puts all quantifiers at the front of the formula.
前束范式把所有量词都放到公式的最前面。
After converting the statement into prenex normal form, we can apply Skolemization and then proceed with resolution more systematically.
把该命题转换为前束范式后，我们可以进行 Skolem 化，再更系统地使用归结法进行推理。
prenex 来自拉丁语词根：*prae-*（“在前、预先”）+ nectere（“连接、系结”），字面含义接近“把（东西）系在前面”。在逻辑中用来描述“把量词都连接到最前端”的结构；normal form 则表示“规范形式/标准形式”，指便于比较、推理或算法处理的统一表达。
Select Language