Skolem 范式
| Skolem范式 | |
|---|---|
| 术语名称 | Skolem范式 |
| 英语名称 | Skolem normal form |
Skolem范式(Skolem normal form)指在前束范式基础上，将存在量词消除为个体常项或全称约束变元的函项，只留下全称量词的形式。与原公式有相同可满足性，但未必等值。
定义
对前束范式 [math]\displaystyle{ \mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n \phi }[/math] ，对 [math]\displaystyle{ \mathsf{Q}_i }[/math] 中的每个存在量词，将其作用变元的每个约束出现替换为其前方每个全称量词所作用的变元的函数，特别地，若前方没有出现全称量词，则替换为一个个体常项，这一过程称为 Skolem 化(Skolemization)。公式的前束范式 Skolem 化的结果称为其 Skolem 范式(Skolem normal form)。
性质
每个谓词公式都有对应的 Skolem 范式，两公式等可满足性。