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.

La regla de resolución sólo se puede aplicar en expresiones en forma clausular. Las premisas y la conclusión deben convertirse a esta forma.

Definición

Una fórmula está en forma normal conjuntiva (FNC) syss es una conjunción de disyunción de literales.

Forma Normal Conjuntiva

• $$(\neg p \lor q\lor r) \land (\neg q \lor r) \land (\neg r)$$

• La fórmula anterior, sí está en FNC.
  
  

• $$(\neg p \lor q\lor r) \land ((p \land \neg q )\lor r) \land (\neg r)$$

• La fórmula anterior, no está en FNC.
  
  

• $$(\neg p \lor q\lor r) \land \neg(\neg q \lor r) \land (\neg r)$$

• La fórmula anterior, no está en FNC.

Definición

• Una literal es una proposición atómica o la negación de una proposición atómica.
• Sea $\ell$ una literal, $\ell$ y $\ell^c$ son literales complementarias, donde

$$\ell^c = \begin{cases} p & \text{si $\ell=\neg p$} \\ \neg p & \text{si $\ell=p$} \end{cases}$$

• 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 ($\square$) es una cláusula y equivale a una disyunción vacía; por lo tanto, es insatisfacible.
• 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. Esto indica que la forma clausular es una conjunción de cláusulas.

La fórmula en FNC

$$(\neg p \lor q\lor r) \land (\neg q \lor r) \land (\neg r)$$

corresponde en forma clausular a $\{ \{\neg p, q, r\}, \{\neg q, r\}, \{\neg r\} \}$.

Teorema

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.

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

$$\begin{array}{lcl} \varphi \rightarrow \psi &\equiv& \neg\varphi \vee\psi\\ \varphi\leftrightarrow\psi &\equiv& (\neg\varphi\vee\psi) \wedge (\varphi\vee\neg\psi) \end{array}$$

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

$$\begin{array}{lcl} \neg\neg\varphi &\equiv & \varphi\\ \neg(\varphi\wedge\psi) &\equiv& \neg\varphi\vee\neg\psi\\ \neg(\varphi\vee\psi) &\equiv& \neg\varphi\wedge\neg\psi \end{array}$$

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

$$\begin{array}{lcl} \varphi\vee(\psi\wedge\chi) &\equiv & (\varphi\vee\psi)\wedge(\varphi\vee\chi)\\ (\varphi\wedge\psi)\vee\chi &\equiv & (\varphi\vee\chi)\wedge(\psi\vee\chi) \end{array}$$

• Ocupar la notación para la forma clausular.

$$\begin{array}{lcl} \varphi_1\vee\ldots\vee\varphi_n &\rightsquigarrow & \{\varphi_1,\ldots,\varphi_n\}\\ \psi_1\wedge\ldots\wedge\psi_m &\rightsquigarrow & \{\psi_1,\ldots,\psi_m\}\\ \end{array}$$

Este paso genera conjuntos, así que se eliminan duplicados. La equivalencia se preserva por idempotencia: $\varphi\wedge\varphi\equiv\varphi$ y $\varphi\vee\varphi\equiv\varphi$

Cláusula trivial

Definición

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

Lema

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$.

Resolución

• Proporciona un método de demostración que utiliza el Principio de Refutació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, también lo es el conjunto que resulta de la aplicación de la regla.
• Si se obtiene la cláusula vacía (insatisfacible), el conjunto original de cláusulas es insatisfacible.

Regla de resolución

$$\dfrac{C_1\qquad C_2}{(C_1-\{\ell\}) \cup (C_2-\{\ell^c\})}\;\; (\mathsf{Res})$$

Las cláusulas padre son $C_1$ y $C_2$, el resolvente es $C$

$$C=(C_1-\{\ell\}) \cup (C_2-\{\ell^c\})$$

Algunos ejemplos

$$\dfrac{C_1\qquad C_2}{(C_1-\{\ell\}) \cup (C_2-\{\ell^c\})}$$

$$\dfrac{\{p,q,\neg r\}\qquad \{r, s, \neg t\}}{\{p,q, s, \neg t\}}$$

Algunos ejemplos

$$\dfrac{C_1\qquad C_2}{(C_1-\{\ell\}) \cup (C_2-\{\ell^c\})}$$

$$\dfrac{\{\neg p,q\}\qquad \{\neg q\}}{\{\neg p\}}$$

Algunos ejemplos

$$\dfrac{C_1\qquad C_2}{(C_1-\{\ell\}) \cup (C_2-\{\ell^c\})}$$

$$\dfrac{\{p,q,\neg r\}\qquad \{\neg p, r, s\}}{\{p,q, \neg p, s\}}$$

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

Si $C_1$ y $C_2$ colisionan en más de una literal, su resolvente es una cláusula trivial.

Algunos ejemplos

$$\dfrac{C_1\qquad C_2}{(C_1-\{\ell\}) \cup (C_2-\{\ell^c\})}$$

$$\dfrac{\{s\}\qquad \{\neg s\}}{\square}$$

Algunos ejemplos

$$\dfrac{\{s\}\qquad \{\neg s\}}{\square}$$

• La cláusula vacía es una disyunción entre elementos nulos, ¡uno de ellos debe satisfacerse para que $\square$ también se satisfaga!
• La cláusula vacía se satisface siempre que $s$ y $\neg s$ se satisfagan.
• La cláusula vacía es insatisfasible.

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

• $\boxed{\rightarrow}$ Sea $I$ una interpretación que satisface a $C$, $I(\ell^{\diamond})=1$ para al menos alguna literal $\ell^{\diamond}\in C$.
• Si $\ell^{\diamond}\in C_1$, $I(C_1)=1$.
• Como $\ell\not\in C$ ni $\ell^c\not\in C$, $I$ no está definida en $\ell$ o $\ell^c$. Extendemos $I$ a $I'$ definiendo $I'(\ell^c)=1$. Puesto que $\ell^c\in C_2$, tenemos $I'(C_2)=1$; además $I'(C_1)=I(C_1)=1$.
• Por lo tanto, $I'$ es un modelo para $C_1$ y $C_2$. Análogamente cuando $\ell^{\diamond}\in C_2$.

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

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

Algoritmo (resolución binaria)

Input: Un conjunto de cláusulas $S$.
Output: $S$ es satisfacible o insatisfacible.

Definimos $S_0=S$.

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

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

Algoritmo (resolución binaria. Continuación.)

• Encuentre $C=\mathsf{Res}(C_1, C_2)$ de acuerdo a la regla de resolución.
• Si $C$ no es una cláusula trivial, $S_{i+1}=S_i\cup\{C\}$; de otro modo, $S_{i+1}=S_i$.

Hasta que $C=\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.

Proposición

Si un conjunto de cláusulas $S=\{\varphi_1,\varphi_2,\ldots,\varphi_n\}$ ($n\geq 0)$ es satisfacible, entonces cualquier conjunto $S_i$ ($i\geq 0$), generado por el algoritmo de resolución binaria, es satisfacible.