查看“︁Skolem 范式”︁的源代码

[[分类:谓词逻辑]]
{{InfoBox
|name=Skolem范式
|eng_name=Skolem normal form
}}
'''<ins>Skolem</ins>范式'''('''Skolem normal form''')指在[[前束范式]]基础上，将[[存在量词]]消除为[[个体词（谓词逻辑）|个体常项]]或全称约束变元的[[函项]]，只留下[[全称量词]]的形式。与原公式有相同可满足性，但未必等值。

== 定义 ==

对前束范式 <math>\mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n \phi</math> ，对 <math>\mathsf{Q}_i</math> 中的每个存在量词，将其作用变元的每个约束出现替换为其前方每个全称量词所作用的变元的函数，特别地，若前方没有出现全称量词，则替换为一个个体常项，这一过程称为 '''Skolem 化'''('''Skolemization''')。公式的前束范式 Skolem 化的结果称为其 '''Skolem 范式'''('''Skolem normal form''')。

== 性质 ==

每个谓词公式都有对应的 Skolem 范式，两公式等可满足性。


{{谓词逻辑}}