•Eliminação dos quantificadores existenciais (Skolemização ou Funções de Skolem)
–Quando uma fórmula está na forma normal Prenex, pode-se eliminar os quantificadores existenciais por uma função, se as variáveis estiverem no escopo do quantificador universal; caso estejam fora, substitui-se por uma constante.
–As constantes e funções usadas para substituir as variáveis existenciais são chamadas constante e funções de Skolem
•Ex.: "x $ y P(x,y)
•           Skolemizando: "x P(x,f(x))
•onde f(x) tem por único propósito garantir que existe algum valor (y) que depende de x pois está dentro do seu escopo. No entanto, se o quantificador existencial não residir no escopo  do quantificador universal, como em $ y "x P(x,y), a variável quantificada existencialmente será substituída por uma constante  "x P(x,a) que assegure sua existência, assim como sua independência de qualquer outra variável.
–Por fim, abandona-se os quantificadores pré-fixados, e obtém-se uma sentença na forma CLAUSAL.
–CLÁUSULA: É uma disjunção de literais
•