查看“︁前束范式”︁的源代码

[[分类:谓词逻辑]]
{{InfoBox
|name=前束范式
|eng_name=prenex normal form
|aliases=PNF
}}
'''前束范式'''('''prenex normal form''', '''PNF''')指[[谓词公式]]的一种形式，将全部[[量词|量化表达式]]都放在最前面，且这些量词均非否定无取值范围、辖域都覆盖到公式尾部。

== 定义 ==

对谓词公式，若其具有形式 <math>\mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n \phi</math> ，其中 <math>\phi</math> 不含量词，量词 <math>\mathsf{Q}_i \in \langle \forall, \exists \rangle</math> 且每个约束变项 <math>x_i</math> 均有在 <math>\phi</math> 中的出现，则称其为一个'''前束范式'''('''prenex normal form''', '''PNF''')。其中 <math>\mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n</math> 称为'''首标'''('''prefix''')， <math>\phi</math> 称为'''母式'''/'''基式'''('''matrix''')。

对谓词公式 <math>\psi</math> ，若有一前束范式与其逻辑等值，则称其为公式 <math>\psi</math> 的一个'''前束范式'''。

注：有的定义不要求约束变项均有出现。

== 前束范式存在定理 ==

对每个公式 <math>\psi</math> ，都存在一个前束范式 <math>\phi</math> 与其逻辑等值。

=== 构造证明 ===

* 消去联结词 <math>\rightarrow, \leftrightarrow</math> 。
* 深化否定词到否定表达式
* 进行易字以免冲突
* 量词前移，使辖域覆盖全公式


{{谓词逻辑}}