Una fórmula de la lógica de primer orden se considera expresada en forma normal de Skolem si su forma normal prenexa solamente contiene cuantificadores universales.
Una fórmula puede ser Skolemizada, lo que implica que sus cuantificadores existenciales son suprimidos, produciendo una nueva fórmula equisatisfactible con respecto a la original.
[1] La skolemización es una aplicación de la equivalencia (aplicación perteneciente a la lógica de segundo orden).
Para encontrar la forma normal de Skolem de cualquier fórmula se siguen los pasos siguientes: El punto álgido a la hora de encontrar la forma normal de Skolem de una fórmula es la eliminación de los cuantificadores existenciales, esta eliminación es conocida como skolemización.
Para ello solo es necesario adaptar la forma normal skolemizada a la peculiaridades de este método.