Lógica Computacional
Nota 05. Resolución binaria

1 Introducción

El método de resolución encuentra de manera eficiente una demostración de una fórmula a partir de las premisas mediante la regla de resolución, con la cual es posible construir un demostrador de teoremas que sea correcto y completo para la lógica proposicional. Las ventajas de este método serán aparentes hasta que se extienda a la lógica de primer orden.

La regla de resolución sólo se puede aplicar en expresiones en forma clausular. Antes de la aplicación, las premisas y la conclusión deben convertirse a esta forma. Afortunadamente, hay un proceso sencillo para realizar esta transformación.

Definición 1.1

  

• Una literal es una proposición atómica o la negación de una proposición atómica.

• Sea $\mathrm{\ell }$ una literal, $\mathrm{\ell }$ y ${\mathrm{\ell }}^c$ son literales complementarias, donde

• Una oración clausular es una literal o una disyunción de literales.

• Una cláusula es el conjunto de literales en una oración clausular. Observe que el conjunto vacío de literales es una cláusula y equivale a una disyunción vacía; por lo tanto, es insatisfacible, se denota como $\mathrm{\square }$, y es un caso especial particularmente importante.

• La cláusula unitaria es una cláusula que consiste en una sola literal.

• Una fórmula en forma clausular es un conjunto de cláusulas. Implícitamente, esto indica que la forma clausular es una conjunción de cláusulas.

Teorema 1.2

Toda fórmula de la lógica proposicional puede ser transformada en una fórmula equivalente en forma clausular.

Demostración. Para convertir una fórmula a su forma clausular se llevan a cabo los siguientes pasos, cada uno de los cuales preserva la equivalencia lógica.

1. Eliminar implicaciones y bicondicionales al sustituirlas por la fórmulas equivalentes.

2. Trabajar con la negación de modo que se aplique únicamente sobre proposiciones atómicas atómicas.

3. Aplicar las leyes de la distributividad para eliminar conjunciones dentro de disyunciones.

4. Ocupar la notación para la forma clausular.

El último paso de la demostración genera conjuntos, lo que causa que múltiples presencias de una cláusula se colapsen en una sola. La equivalencia lógica se preserva por idempotencia: $\phi \wedge \phi \equiv \phi$ y $\phi \vee \phi \equiv \phi$. $\mathbf{⊣}$

1.1 Cláusula trivial

Definición 1.3

Una cláusula es trivial si contiene un par de literales complementarias. Se llama así porque trivialmente se satisface.

Lema 1.4

Sea $S$ un conjunto de cláusulas y sea $C\in S$ una cláusula trivial. Entonces $S-\{C\}$ es lógicamente equivalente a $S$.

Por lo tanto, asumiremos que todas las cláusulas triviales han sido eliminadas de las fórmulas en forma clausular.

Ejercicios 1.5

• Encuentra la Forma Normal Clausular para las siguientes fórmulas:

  • $(\neg p\to \neg q)\to (p\to q)$

  • $\neg (\neg q\leftrightarrow r)$

  • $p\wedge q\to r\vee s$

  • $p\wedge q\leftrightarrow r$

• Decidir si la fórmula $(p\vee q)\leftrightarrow (\neg p\to q)$ es válida utilizando la transformación a la Forma Normal Clausular.

2 Resolución

La resolución binaria proporciona un método de decisión para la lógica que utiliza el principio de refutación. El procedimiento de resolución consiste en una secuencia de aplicaciones de la regla de resolución sobre un conjunto de cláusulas. La regla preserva satisfacibilidad: si un conjunto de cláusulas es satisfacible, lo es también el conjunto de cláusulas que se genera por la aplicación de la regla. Por lo tanto, si la cláusula vacía (insatisfacible) se llega a obtener, el conjunto original de cláusulas debe ser insatisfacible.

Definición 2.1 (Regla de resolución)

Sean $C_1$ y $C_2$ dos cláusulas con $\mathrm{\ell }\in C_1$ y ${\mathrm{\ell }}^c\in C_2$. Decimos que $C_1$ y $C_2$ son cláusulas de colisión y que colisionan en el par de literales complementarias $\mathrm{\ell }$ y ${\mathrm{\ell }}^c$. Obtenemos la cláusula $C$, el resolvente de $C_1$ y $C_2$, como sigue:

$$C=\mathrm{𝖱𝖾𝗌}(C_1,C_2)=(C_1-\{\mathrm{\ell }\})\cup (C_2-\{{\mathrm{\ell }}^c\}).$$

Podemos expresar esta relación al estilo de una regla de inferencia del siguiente modo,

$$\frac{C_1{C}_2}{(C_1-\{\mathrm{\ell }\})\cup (C_2-\{{\mathrm{\ell }}^c\})}(\mathrm{𝖱𝖾𝗌})$$

$C_1$ y $C_2$ son las cláusulas padre de $C$.

Es importante mencionar que las cláusula vacía o cláusula insatisfacible, $\mathrm{\square }$, se obtiene como resultado de $\mathrm{𝖱𝖾𝗌}(\{\mathrm{\ell }\},\{{\mathrm{\ell }}^c\})$.

La regla opera sobre un par de literales complementaras a la vez y nunca con más.

Lema 2.2

Una disyunción de literales ${\mathrm{\ell }}_1\vee \mathrm{\dots }\vee {\mathrm{\ell }}_m$ es válida syss existen $1\le i,j\le m$ tal que ${\mathrm{\ell }}_i$ es $\neg {\mathrm{\ell }}_j$.

Lema 2.3

Si dos cláusulas colisionan en más de una literal, su resolvente es una cláusula trivial.

Teorema 2.4

El resolvente $C$ es satisfacible syss las cláusulas padre $C_1$ y $C_2$ son ambas satisfacibles.

Demostración. $\boxed{\to }$ Sea $I$ una interpretación que satisface a $C$, entonces $I({\mathrm{\ell }}^{\diamond })=1$ para al menos alguna literal en ${\mathrm{\ell }}^{\diamond }\in C$. Por la regla de resolución, ${\mathrm{\ell }}^{\diamond }\in C_1$ o ${\mathrm{\ell }}^{\diamond }\in C_2$, o en ambos. Si ${\mathrm{\ell }}^{\diamond }\in C_1$, $I(C_1)=1$. Ahora, $\mathrm{\ell }\notin C$ ni ${\mathrm{\ell }}^c\notin C$, por lo que $I$ no está definida en $\mathrm{\ell }$ o ${\mathrm{\ell }}^c$, así que extendemos $I$ como $I^{\prime }$ definiendo $I^{\prime }({\mathrm{\ell }}^c)=1$. Como ${\mathrm{\ell }}^c\in C_2$, tenemos $I^{\prime }(C_2)=1$; además $I^{\prime }(C_1)=I(C_1)=1$. Por lo tanto, $I^{\prime }$ es un modelo para $C_1$ y $C_2$. Análogamente cuando ${\mathrm{\ell }}^{\diamond }\in C_2$.

$\boxed{\leftarrow }$ Sean $C_1$ y $C_2$ satisfacibles por la interpretación $I$. Como $\mathrm{\ell }$ y ${\mathrm{\ell }}^c$ son complementarias, se tiene que $I(\mathrm{\ell })=1$, o bien, $I({\mathrm{\ell }}^c)=1$. Supongamos que $I(\mathrm{\ell })=1$, entonces $I({\mathrm{\ell }}^c)=0$ y $C_2$, la cláusula que contiene a ${\mathrm{\ell }}^2$, se satisface porque hay otra literal ${\mathrm{\ell }}^{\prime }\in C$ (${\mathrm{\ell }}^{\prime }\ne {\mathrm{\ell }}^c$) tal que $I({\mathrm{\ell }}^{\prime })=1$. Por construcción de la regla de resolución, ${\mathrm{\ell }}^{\prime }\in C$, de modo que $I$ también es un modelo de $C$. Análogamente cuando $I({\mathrm{\ell }}^c)=1$.

Lema 2.5

La cláusula vacía, $\mathrm{\square }$, es insatisfacible. El conjunto vacío de cláusulas, $\mathrm{\varnothing }$, es válido.

Demostración. Una cláusula es satisfacible syss hay alguna interpretación bajo la cual al menos una literal en la cláusula es verdadera. Sea $I$ una interpretación arbitraria. Como no hay literales en $\mathrm{\square }$, no hay literales cuyo valor sea verdadero bajo $I$. Pero $I$ es una interpretación arbitraria; por consiguiente, $\mathrm{\square }$ es insatisfacible.

También se puede ver a $\mathrm{\square }$ como el resolvente de las cláusulas padre $\{\mathrm{\ell }\}$ y $\{{\mathrm{\ell }}^c\}$. Como el teorema anterior establece, $\mathrm{\square }$ es satisfacible syss $\{\mathrm{\ell }\}$ y $\{{\mathrm{\ell }}^c\}$ son satisfacibles, pero no se puede satisfacer a un par de literales complementarias. Por lo tanto, $\mathrm{\square }$ es insatisfacible.

Un conjunto de cláusulas es satisfacible syss toda cláusula en él es verdadera para cualquier interpretación. Como no hay cláusulas en $\mathrm{\varnothing }$ que requieran ser verdaderas, entonces $\mathrm{\varnothing }$ es válido. $\mathbf{⊣}$

2.1 Algoritmo de resolución binaria

Algoritmo (Resolución binaria)

Input: Un conjunto de cláusulas $S$.

Output: $S$ es satisfacible o insatisfacible.

Sea $S$ un conjunto de cláusulas. Definimos $S_0=S$.

Repetir los siguientes pasos para obtener $S_{i+1}$ a partir de $S_i$:

• Escoja un par de cláusulas de colisión $\{C_1,C_2\}\subseteq S_i$ que no se hayan escogido anteriormente.

• Encuentre el resolvente $C=\mathrm{𝖱𝖾𝗌}(C_1,C_2)$ de acuerdo a la regla de resolución.

• Si $C$ no es una cláusula trivial, definimos $S_{i+1}=S_i\cup \{C\}$; de otro modo, $S_{i+1}=S_i$.

Hasta que $C=\mathrm{\square }$, en cuyo caso $S$ es insatisfacible; o hasta que la regla de resolución se haya aplicado a todos los pares de cláusulas de colisión, lo que indica que $S$ es satisfacible.

Ejercicios 2.6

• Decida si los siguientes argumentos lógicos son correctos por resolución binaria.

  • $\{\mathrm{\ell }\vee m\to h,\neg (\neg h\wedge \neg m)\}\vDash h$

  • $\{p\vee (q\wedge r),p\to q,q\leftrightarrow s\}\vDash q\wedge s$

  • $\{p\to q,r\vee s\to t,t\to p\}\vDash p\to (\neg r\wedge s)$

  • Una condición necesaria para que llueva es que sea primavera o invierno. Si hay ríos, entonces llueve. Si es invierno, la gente utiliza gorros azules. La gente no utiliza gorros azules y hay ríos. Por lo tanto, es primavera. Utilice las claves:

• Determine si los siguientes conjuntos son satisfacibles o no.

  • $\{p\wedge \neg (q\to s),p\vee q,s\leftrightarrow \neg p\}$

  • $\{p,p\to \left((q\vee r)\wedge \neg (q\wedge r)\right),p\to \left((s\vee t)\wedge \neg (s\wedge t)\right),s\to q,\neg r\to t,t\to s\}$

2.2 Correctud y completud

Teorema 2.7 (Correctud)

Sea $S$ un conjunto de cláusulas. Si existe una refutación por resolución para $S$, entonces $S$ es insatisfacible.

Teorema 2.8 (Completud)

Si un conjunto de cláusulas es insatisfacible, entonces la cláusula vacía $\mathrm{\square }$ será derivada por el procedimiento de resolución.

3 Ejemplo

Decida si $\{p\to q,r\to s,p\vee r,\neg (q\wedge s)\}\vDash (q\to p)\wedge (s\to r)$ es correcto por resolución binaria.

Por el principio de refutación, vamos a trabajar con

$$\{p\to q,r\to s,p\vee r,\neg (q\wedge s),\neg ((q\to p)\wedge (s\to r))\}$$

Primero pasamos las fórmulas anteriores a forma clausular.

Aplicando resolución tenemos lo siguiente: En azul están todos los resolventes que obtenemos de aplicar resolución a las premisas. En rojo aquellos que ocupan de las premisas y de los resolventes en azul. Esta forma esquemática permite saber si ya se ha aplicado resolución a todos los pares de cláusulas de colisión. Ahora se encuentran resolventes entre las premisas y las cláusulas en rojo, lo cual produce la cláusula 29, y finalmente llegamos a la cláusula vacía en la 30.

Como se obtuvo la cláusula vacía, el conjunto de fórmulas es insatisfacible. Por consiguiente, el argumento es correcto.