Demostración de la insatisfactibilidad con resolución proposicional

Question

Tengo problemas para entender cómo utilizar la regla de resolución para demostrar si una afirmación es satisfactible o insatisfactible.

He visto esta clase del curso sobre resolución proposicional e insatisfacción (enlazada con una marca de tiempo para saltar a la parte en cuestión):
"5.4 - Método de Resolución - Resolución Proposicional - [Introducción A La Lógica] Por Michael Genesereth" https://www.youtube.com/watch?v=IpixwNupBIs#t=2m21s

Para los que no quieran ver el vídeo, lo que yo entiendo es que dice que para un enunciado en forma normal conjuntiva (CNF) podemos comprobar si el enunciado es satisfacible aplicando repetidamente la regla de resolución simplificadora:
Si hay un par de cláusulas de la forma $$(a \vee X)$$ $$(\neg a \vee Y)$$ puede sustituirse por una única cláusula $$(X \vee Y)$$

La afirmación es que un enunciado es insatisfactible si y sólo si la aplicación repetida de esta regla conduce a una cláusula vacía.

Pero esto no tiene sentido para mí. Creo que hay algunos detalles importantes que se omiten. Por ejemplo, en el ejemplo del vídeo, considere la afirmación con las cláusulas

1. $(p \vee q)$
2. $(p \vee \neg q)$
3. $(\neg p \vee q)$
4. $(\neg p \vee \neg q)$

Por inspección, esto es insatisfactorio. Pero encontremos esto usando la regla de resolución, siguiendo con el video...

Aplicando la regla de resolución al par 1,2 se obtiene: $p$

Entonces aplicando la regla de resolución sobre el par 3,4 se obtiene $\neg p$

Así que ahora sólo tenemos las cláusulas $p, \neg p$ que después de aplicar la regla de resolución una vez más da la cláusula vacía.

Así es como va el ejemplo en el vídeo. Pero mira lo que pasa si aplicamos la regla en otro orden:

Aplicando la regla de resolución al par 1,4 se obtiene: $q \vee \neg q$

Entonces aplicando la regla de resolución sobre el par 2,3 se obtiene $\neg q \vee q$

Así que ahora sólo nos quedan dos cláusulas que son tautologías. Así que simplificamos el enunciado a $\top$ . Así que por este orden, afirma que el enunciado es satisfacible.

Está claro que algo va mal. ¿Qué he entendido mal? ¿O es que la lección del curso omite algo crucial?

Answer 1

Puede ver :

• Melvin Fitting, Lógica de primer orden y demostración automatizada de teoremas (1990), Cap. 3.3 Resolución proposicional página 45

para un tratamiento completo del sistema de pruebas basado en la Norma de resolución .

El sistema de pruebas "amplía" el conjunto de cluases, aplicando la Regla de Resolución para añada a nueva cláusula (una disyunción) al conjunto original de cláusulas. La regla tiene la propiedad de "preservar la satisfacibilidad", es decir, el nuevo conjunto de cláusulas es satisfacible si el original lo es.

Así, si tras aplicaciones iteradas de la regla el cláusula vacía se produce, siendo ésta insatisfactible (es otra forma de escribir $\bot$ es decir, a contradicción ) esto es suficiente para concluir que también el conjunto original de cláusulas es insatisfactible.

Answer 2

Creo que este algoritmo debería ayudarte . Tienes que añadir la cláusula resuelta a tu conjunto de cláusulas cada vez que resuelves y así tu conjunto de cláusulas crece. Además, antes de añadir, tienes que asegurarte de que cuando resuelves no acabas generando la cláusula que podrías haber generado antes en el proceso de resolución o (que ya existe en tu conjunto de cláusulas). Mira las imágenes del algoritmo

Insatisfacción algo pic

Saturación Algo pic