考虑一个前束范式公式，
 |
如果 
是存在量词 (
) 且 
, ..., 
是所有全称量词变量，使得 
, 
，那么引入新的函数符号 
和项 
。(如果 
，那么 
是一个常数。) 这个函数被称为 Skolem 函数（或 Herbrand 函数）。
现在将所有出现的 
替换为这个项，并移除 
。当所有存在量词被移除后，将 
转换为合取范式。这个过程，通常被称为 Skolem 化，会得到一个Skolem 化形式的公式。结果公式是不可满足的当且仅当源公式是不可满足的。注意，如果源公式是可满足的，它不一定等价于结果公式。
