前束范式
| 前束范式 | |
|---|---|
| 术语名称 | 前束范式 |
| 英语名称 | prenex normal form |
| 别名 | PNF |
前束范式(prenex normal form, PNF)指谓词公式的一种形式，将全部量化表达式都放在最前面，且这些量词均非否定无取值范围、辖域都覆盖到公式尾部。
定义
对谓词公式，若其具有形式 [math]\displaystyle{ \mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n \phi }[/math] ，其中 [math]\displaystyle{ \phi }[/math] 不含量词，量词 [math]\displaystyle{ \mathsf{Q}_i \in \langle \forall, \exists \rangle }[/math] 且每个约束变项 [math]\displaystyle{ x_i }[/math] 均有在 [math]\displaystyle{ \phi }[/math] 中的出现，则称其为一个前束范式(prenex normal form, PNF)。其中 [math]\displaystyle{ \mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n }[/math] 称为首标(prefix)， [math]\displaystyle{ \phi }[/math] 称为母式/基式(matrix)。
对谓词公式 [math]\displaystyle{ \psi }[/math] ，若有一前束范式与其逻辑等值，则称其为公式 [math]\displaystyle{ \psi }[/math] 的一个前束范式。
注：有的定义不要求约束变项均有出现。
前束范式存在定理
对每个公式 [math]\displaystyle{ \psi }[/math] ，都存在一个前束范式 [math]\displaystyle{ \phi }[/math] 与其逻辑等值。
构造证明
- 消去联结词 [math]\displaystyle{ \rightarrow, \leftrightarrow }[/math] 。
- 深化否定词到否定表达式
- 进行易字以免冲突
- 量词前移，使辖域覆盖全公式