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 范式，两公式等可满足性。

谓词逻辑/一阶逻辑
命题结构	项	个体词（个体常项、个体变项）、论域/个体域、函项、项、闭项
	谓词	谓词（谓词常项、谓词变项）
	量词	量词（辖域、出现）、全称量词 [math]\displaystyle{ \forall }[/math] 、存在量词 [math]\displaystyle{ \exists }[/math]
谓词公式	形式定义	谓词语言 [math]\displaystyle{ \mathcal{L}^* }[/math] 、谓词公式、闭式
	逻辑语义	结构、指派/赋值、基本语义定义、解释、满足、模型
	语义分类	普遍有效公式、可满足式、不可满足式
	语义关系	逻辑等值/逻辑等价 [math]\displaystyle{ = }[/math]/[math]\displaystyle{ \Leftrightarrow }[/math] 、逻辑蕴涵 [math]\displaystyle{ \Rightarrow }[/math]
	范式	前束范式、 Skolem 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理