Método de Resolución en Lógica: Procedimientos para Satisfactibilidad y Validez

0ºº

Esquema Universal de Resolución

Planteamiento Inicial

• Si piden Satisfactibilidad: "Para evaluar la satisfactibilidad de $F$, aplicaremos el método de resolución sobre la propia fórmula original."
• Si piden Validez: "Para demostrar la validez de $F$ mediante resolución (reducción al absurdo), procedemos a evaluar la insatisfactibilidad de su negación: $\neg F$."

Conversión a Forma Normal Conjuntiva (FNC)

Detalle cada paso aplicando una sola regla lógica por línea para evitar penalizaciones.

• [Fórmula a evaluar] (Fórmula inicial)
• [Fórmula equivalente] (Eliminación de implicaciones/bicondicionales)
• [Fórmula equivalente] (Leyes de De Morgan y doble negación)
• [Fórmula en FNC] (Propiedad distributiva/asociativa)

Conjunto de Cláusulas (S)

Numere cada cláusula claramente para facilitar su referenciación posterior.

1. [Cláusula 1]
2. [Cláusula 2]
3. [Cláusula N]

Inferencia por Resolución

Muestre solo las resoluciones útiles o las que lleven al final del proceso. Use el formato "Cláusula X + Cláusula Y".

• Resolviendo (X) y (Y) respecto a [literal], obtenemos: [Nuevo Resolvente]. (Añadir como nueva cláusula numerada si no es redundante).
• [Repetir hasta derivar la cláusula vacía o saturar las opciones].

Conclusión (El Veredicto)

Elija estrictamente una de las siguientes cuatro conclusiones según el escenario:

• Escenario A: Piden Satisfactibilidad y NO llega a la cláusula vacía.

  "El proceso de resolución se ha saturado sin derivar la cláusula vacía ($\square$). El conjunto es consistente. Por tanto, la sentencia original es satisfactible."

• Escenario B: Piden Satisfactibilidad y SÍ llega a la cláusula vacía.

  "Se ha derivado la cláusula vacía ($\square$), lo que evidencia una contradicción en el conjunto. Por tanto, la sentencia original es insatisfactible."

• Escenario C: Piden Validez y NO llega a la cláusula vacía.

  "Al aplicar resolución sobre la fórmula negada, el proceso se satura sin derivar la cláusula vacía ($\square$). La negación es satisfactible, lo que implica que existe un contraejemplo. Por tanto, la sentencia original no es válida."

• Escenario D: Piden Validez y SÍ llega a la cláusula vacía.

  "Al aplicar resolución sobre la fórmula negada, se ha derivado la cláusula vacía ($\square$). Esto demuestra que la negación es una contradicción. Por tanto, la sentencia original es una tautología y sí es válida."

Resolución del Ejercicio (Caso Bicondicional)

Planteamiento Inicial

Para demostrar la validez de F mediante resolución (reducción al absurdo), procedemos a evaluar la insatisfactibilidad de su negación: ¬F. Al ser F un bicondicional (A ↔ B), su negación se divide en dos ramas: (A ∧ ¬B) ∨ (¬A ∧ B). Si una sola rama es satisfactible, la fórmula completa no es válida. Evaluaremos la Rama 1 (A ∧ ¬B).

Conversión a Forma Normal Conjuntiva (FNC)

• F_rama1 ≡ ∃x (P(x) → ¬Q(x)) ∧ ¬(¬∃x (P(x) ∧ Q(x))) [Rama 1 inicial a evaluar]
• F_rama1 ≡ ∃x (P(x) → ¬Q(x)) ∧ ¬(¬∃y (P(y) ∧ Q(y))) [Estandarización de variables]
• F_rama1 ≡ ∃x (¬P(x) ∨ ¬Q(x)) ∧ ∃y (P(y) ∧ Q(y)) [Eliminación de implicaciones y doble negación]
• F_rama1 ≡ (¬P(a) ∨ ¬Q(a)) ∧ (P(b) ∧ Q(b)) [Skolemización: sustitución de ∃ independientes por constantes a y b]
• F_rama1 ≡ (¬P(a) ∨ ¬Q(a)) ∧ P(b) ∧ Q(b) [Asociatividad / FNC final]

Conjunto de Cláusulas (S)

1. ¬P(a) ∨ ¬Q(a)
2. P(b)
3. Q(b)

Inferencia por Resolución

• Intentando resolver (1) y (2) respecto a P: La unificación falla estrepitosamente, dado que la constante de Skolem "a" es estrictamente diferente de "b" (a ≠ b). No hay unificador posible.
• Intentando resolver (1) y (3) respecto a Q: La unificación falla por el mismo motivo formal (a ≠ b).
• El motor de inferencia se agota sin posibles cruces válidos.

Conclusión (El Veredicto)

Al aplicar resolución sobre la fórmula negada (rama 1), el proceso se satura sin derivar la cláusula vacía []. La negación es satisfactible, lo que implica que existe al menos un contraejemplo. Por tanto, la sentencia original no es válida.

Resolución para un Condicional (A → B)

Planteamiento Inicial

Para demostrar la validez de la sentencia condicional F ≡ A → B mediante resolución (reducción al absurdo), procedemos a evaluar la insatisfactibilidad de su negación: ¬F. Aplicando la equivalencia de la negación del condicional, operamos directamente sobre un único conjunto unificado: ¬F ≡ ¬(A → B) ≡ A ∧ ¬B.

Conversión a Forma Normal Conjuntiva (FNC)

En este bloque se aplican de forma secuencial y estricta las reglas de la Lógica de Primer Orden:

• ¬F ≡ [A ∧ ¬B] (Fórmula negada inicial)
• ¬F ≡ [ Eliminación de condicionales internos en A y B ]
• ¬F ≡ [ Interiorización de negaciones mediante Leyes de De Morgan ]
• ¬F ≡ [ Estandarización de variables para evitar nombres duplicados ]
• ¬F ≡ [ Skolemización: sustitución de ∃ por constantes (a, b) o funciones (f(x)) ]
• ¬F ≡ [ Eliminación de cuantificadores universales ∀ ]
• ¬F ≡ [ Aplicación de distributividad si fuera necesario para FNC final ]

Conjunto de Cláusulas (S)

Extracción metódica de las cláusulas resultantes:

1. [Cláusula 1]
2. [Cláusula 2]
3. [Cláusula N]

Inferencia por Resolución

Ejecución de los cruces lógicos utilizando unificación:

• Resolviendo las cláusulas (X) y (Y) respecto al literal [Predicado], aplicando el unificador más general σ = {x / a}, obtenemos el resolvente: [Nuevo Resolvente].
• (Repetir el proceso de forma iterativa hasta alcanzar la contradicción o la saturación).

Conclusión (El Veredicto)

• Escenario A (Si se obtiene la cláusula vacía): "Se ha derivado con éxito la cláusula vacía []. Esto demuestra formalmente que el conjunto de cláusulas de la negación es insatisfactible (contradictorio). Por consiguiente, queda demostrado que la sentencia condicional original es válida."
• Escenario B (Si el proceso se satura sin obtenerla): "El proceso de resolución se ha saturado sin que haya sido posible derivar la cláusula vacía []. Por tanto, la negación es satisfactible, lo que invalida la hipótesis. La sentencia condicional original no es válida."