Skolemización

Una transformación sintáctica que elimina cuantificadores existenciales introduciendo funciones o constantes de Skolem, produciendo una fórmula equisatisfiable en la que los existenciales se han suprimido, comúnmente como paso hacia la forma de cláusulas o el razonamiento automático.