¿Qué es?
Es la que se utiliza para poder aplicar, posteriormente, el Resolución (Lógica). Es una Fórmula formal prenexa, con la matriz normalizada (FNC) y con un prefijo que sólo contiene cuantificadores universales. Los cuantificadores existenciales se eliminan siguiendo un proceso denominado eskolemización.
¿Cómo la podemos obtener?
-
Verificar que no existen variables libres. Si la fórmula se ha dado con variables libres, éstas se deben cuantificar existencialmente. Los cuantificadores existenciales que se añadan deberán colocarse a la izquierda del todo de la fórmula.
-
Opcionalmente, si se utiliza el mismo nombre para variables dentro del ámbito de cuantificadores distintos, puede ser útil cambiar estos nombres.
-
Eliminar todas las apariciones de la conectiva "→" (A → B ⊣ ⊢ ¬A ∨ B).
-
Aplicar las leyes de De Morgan para conseguir que las negaciones precedan a los símbolos de predicado.
-
Eliminar los cuantificadores existenciales (eskolemización).
-
Mover todos los cuantificadores* hacia la izquierda.
-
Normalizar la matriz. Para poder aplicar el método de resolución, es necesario que esté expresada en forma normal conjuntiva.