Forma normal de Skolem

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.

La skolemización es una aplicación de la equivalencia (aplicación perteneciente a la lógica de segundo orden).

Cómo encontrar la forma normal de Skolem

Para encontrar la forma normal de Skolem de cualquier fórmula se siguen los pasos siguientes:

  1. Se ha de verificar que en la fórmula a skolemizar no existan variables libres, si estas existieran se han de cualificar existencialmente y el cuantificador existencial se ha de colocar totalmente a la izquierda de la fórmula.
  2. Opcionalmente si en la fórmula aparecen variables con el mismo nombre pero en ámbitos de cuantificadores diferentes es recomendado diferenciarlas.
  3. Las apariciones de la conectiva deben ser eliminadas aplicando la equivalencia deductiva .
  4. Aplicar las leyes de De Morgan hasta conseguir que las negaciones precedan a los símbolos de predicado. Se aplicarán tanto las leyes de De Morgan a los enunciados como a las fórmulas cuantificadas.
  5. Eliminar los cuantificadores existenciales.
  6. Mover a la izquierda de la fórmula todos los cuantificadores universales.
  7. Normalizar a la matriz a la forma normal conjuntiva.
Other Languages