Una expresión está en la Forma Normal de Skolem si es una conjunción finita de literales y todos los cuantificadores son universales.[2]

Para convertir una fórmula a Forma Normal de Skolem es necesario suprimir los cuantificadores existenciales. La fórmula obtenida será equisatisfactible a la anterior.

El algoritmo de skolemización para suprimir los cuantificadores existenciales de una fórmula es el siguiente:

- Se busca el primer cuantificador existencial comenzando por la izquierda.

- Si el cuantificador existencial está al principio, se suprime la variable cuantificada por una nueva constante.

Ejemplo:

ExP(x)

cambia a

P(a)

- Si existen n cuantificadores universales antes del cuantificador existencial, suprimir la variable cuantificada existencialmente por una nueva función de las variables universales.

Ejemplo:

Ax₁Ax₂EyP(x₁,x₂,y)

cambia a

Ax₁Ax₂P(x₁,x₂,f(x₁,x₂)).