¿Qué es Método de resolución y escriba un ejemplo?
Respuestas a la pregunta
Respuesta:
Método de resolución
Para realizar una derivación de una fórmula \alpha a partir de un conjunto \Gamma de premisas por resolución necesitamos considerar lo siguiente:
Debemos convertir las premisas \gamma \in \Gamma y la conclusión \alpha a su FNC (Forma Normal Conjuntiva).
Recuerda: los componentes básicos de las FNC son las literales: variables proposicionales o la negación de variables proposicionales.
Las FNC pueden tener, en general, tres formas básicas:
Una conjunción de literales es una FNC, por ejemplo:
\neg P\wedge S \wedge \neg Q
Una disyunción de literales es una FNC, por ejemplo:
P\vee \neg Q \vee R
Una conjunción de varios enunciados-cláusula (una suma elemental es un enunciado cláusula), es decir, una conjunción de disyunciones de literales, por ejemplo:
(S \vee \neg P)\wedge (\neg R \vee P \vee S)\wedge (\neg P \vee R)\wedge T
Una vez que las premisas y la conclusión han sido transformadas a su FNC, el siguiente paso que debes realizar es transformarlas a cláusulas.
Una cláusula es el conjunto de literales que aparecen en un enunciado-cláusula. Dos enunciados-cláusula se separan por una conjunción, así que sólo forman parte de una misma cláusula las literales que están unidas entre sí por disyunciones. Siguiendo los ejemplos anteriores, los casos posibles son los siguientes:
Una conjunción de literales (\neg P\wedge S \wedge \neg Q), se convierte en:
\{\neg P\} , \{S\}, \{\neg Q\}
Una disyunción de literales P\vee \neg Q \vee R, se convierte en:
\{P, \neg Q, R\}
Una conjunción de disyunciones de literales (S \vee \neg P)\wedge (\neg R \vee P \vee S)\wedge (\neg P \vee R)\wedge T, se convierte en:
\{ S, \neg P\}, \{\neg R, P, S\}, \{\neg P, R\}, \{T\}
Una vez que tienes todo convertido a cláusula debes aplicar la única regla del método de resolución hasta que obtengas la misma cláusula o cláusulas de la conclusión.
La regla de resolución es la siguiente, sean A y B dos cláusulas tales que:
A=\{\alpha_{1},\alpha_{2},...,\alpha_{n}, P\}
B=\{\beta_{1},\beta_{2},...,\beta_{m}, \neg P\}
Se concluye una tercera cláusula C tal que:
C=\{\alpha_{1},\alpha_{2},...,\alpha_{n}, \beta_{1},\beta_{2},...,\beta_{m}\}
Cuando después de k pasos obtienes la misma cláusula o cláusulas de la conclusión has realizado una derivación por resolución de la conclusión a partir del conjunto de premisas.
El método alternativo es la prueba por refutación, que consiste prácticamente de los mismo pasos. La diferencia es que antes de comenzar el proceso de transformación a FNC, debes agregar la negación de la conclusión al conjunto premisas.
Debido al Teorema de no-satisfacibilidad (inconsistencia):
\Gamma \models \alpha si y sólo si \Gamma \cup \{\neg \alpha\} es inconsistente.
Si logramos concluir que el nuevo conjunto de premisas es inconsistente, habremos probado o demostrado que la conclusión inicial sí se sigue lógicamente (tautológicamente en lógica proposicional) del conjunto inicial de premisas.
¿Cómo sabemos que un conjunto es inconsistente usando el método de resolución? Muy fácil. Siguiendo la regla de resolución, ¿Qué concluirías de las siguientes dos cláusulas?:
\{P\}, \{\neg P\}
La regla nos dice que eliminemos aquella literal que en una cláusula se encuentra negada y en otra cláusula aparece sin negar, quedándonos con las literales restantes de ambos conjuntos. Pero en el caso anterior, al eliminar a P y a \neg P no quedaría nada, es decir sólo resta el conjunto vacío: \{\}.
Si llegamos al conjunto vacío después de un número finito de aplicaciones de la regla de resolución habremos probado que el conjunto de cláusulas del que partimos corresponde a un conjunto inconsistente de premisas
Explicación paso a paso: