一阶逻辑的公式是Skolem 范式的，如果它的前束范式只有全称量词。一个公式可以被Skolem 化，就是说消除它的存在量词并生成最初的公式的等价可满足的公式。Skolem 化是如下(二阶的)等价的应用

Skolem 化的本质是对如下形式的公式的观察

它在某个模型中是可满足的，在这个模型必定对于所有的

有某些点 使得

为真，并且必定存在某个函数(选择函数)

使得公式

为真。函数 f 叫做 Skolem 函数。

举例说明:

In mathematical logic, reduction to Skolem normal form (SNF) is a method for removing existential quantifiers from formal logic statements, often performed as the first step in an automated theorem prover.

A formula of first-order logic is in Skolem normal form (named after Thoralf Skolem) if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled "Skolemnization"). The resulting formula is not necessarily equivalent to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is satisfiable.