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 ${\displaystyle \rightarrow }$ deben ser eliminadas aplicando la equivalencia deductiva ${\displaystyle A\rightarrow B\leftrightarrow \lnot A\lor B}$.
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.

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. Las reglas básicas para realizar la skolemización son:

1. Si un cuantificador existencial no se encuentra dentro del ámbito de ningún cuantificador universal, se sustituye la variable cuantificada existencialmente por una constante que aún no haya sido utilizada y el cuantificador existencial es eliminado. La constante utilizada no puede volver a ser reutilizada. Por ejemplo, ${\displaystyle \exists xP(x)}$ puede ser cambiado a P(c), donde c es una nueva constante.
2. Si un cuantificador existencial se encuentra dentro del ámbito de un cuantificador universal, se ha de sustituir la variable cuantificada existencialmente por una función de la variable cuantificada universalmente y se elimina el cuantificador existencial. La función no puede haber sido utilizada previamente ni podrá utilizarse posteriormente. Por ejemplo, la fórmula ${\displaystyle \forall x\exists y\forall z.P(x,y,z)}$ no está en forma normal de Skolem porque ella contiene un cuantificador existencial ${\displaystyle \exists y}$. La skolemización reemplaza ${\displaystyle y}$ con ${\displaystyle f(x)}$, donde ${\displaystyle f}$ es un nuevo símbolo de función, y elimina la cuantificación existencial sobre ${\displaystyle y}$. La fórmula resultante es ${\displaystyle \forall x\forall z.P(x,f(x),z)}$. El término Skolem ${\displaystyle f(x)}$ contiene ${\displaystyle x}$ pero no ${\displaystyle z}$ porque el cuantificador a ser eliminado ${\displaystyle \exists y}$ está en el ámbito de ${\displaystyle \forall x}$ pero no en el ámbito de ${\displaystyle \forall z}$; debido a que la fórmula está en forma normal prenexa, esto es equivalente a decir que, en la aparición de los cuantificadores, ${\displaystyle x}$ precede ${\displaystyle y}$ mientras ${\displaystyle z}$ no. La fórmula obtenida por esta transformación es satifactible si y solo si la fórmula original lo es.
3. Si un cuantificador existencial se encuentra dentro del ámbito de más de un cuantificador universal se sustituirá la variable cuantificada existencialmente por una función de todas las variables afectadas por estos cuantificadores universales y se elimina el cuantificador existencial. La función no puede haber sido utilizada previamente ni podrá utilizarse posteriormente.

Uno de los usos de la skolemización es aplicarlo en el método de resolución de la lógica de predicados. Para ello solo es necesario adaptar la forma normal skolemizada a la peculiaridades de este método.

El método de resolución de la lógica de predicados se basa en:

1. Una única regla: la de resolución.
2. Una única estrategia: la reducción al absurdo.
3. La utilización de la forma normal de Skolem (FNS) con la matriz en forma normal conjuntiva (FNC ).
4. La utilización del replanteamiento de la última decisión para garantizar la sistematicidad.
5. El cálculo de sustituciones y el algoritmo de unificación.

Lògica de predicats de Enric Sesa i Nogueras.