考慮一個前束正規化公式，
 |
如果 
是存在量詞 (
) 且 
, ..., 
是所有全稱量詞變數，使得 
, 
，那麼引入新的函式符號 
和項 
。(如果 
，那麼 
是一個常數。) 這個函式被稱為 Skolem 函式（或 Herbrand 函式）。
現在將所有出現的 
替換為這個項，並移除 
。當所有存在量詞被移除後，將 
轉換為合取正規化。這個過程，通常被稱為 Skolem 化，會得到一個Skolem 化形式的公式。結果公式是不可滿足的當且僅當源公式是不可滿足的。注意，如果源公式是可滿足的，它不一定等價於結果公式。
