El método de resolución

La clase sobre la semántica de la lógica proposicional mostró que la validez y la satisfacibilidad son decidibles por la tabla de verdad, a un costo que se duplica con cada variable, y anunció métodos que no exigieran recorrerla. La clase sobre consecuencia y equivalencia semántica redujo toda consecuencia a una insatisfacibilidad: $\Gamma \models \varphi$ si y solo si $\Gamma \cup \{\neg\varphi\}$ es insatisfacible. Las clases sobre las formas normales y sobre su algoritmo dieron a toda fórmula una forma conjuntiva, cuya validez se ve a simple vista, pero cuya satisfacibilidad no se ve. Si esto es así, falta un procedimiento que decida la insatisfacibilidad de una conjunción de cláusulas operando sobre las cláusulas mismas. Ese procedimiento es la resolución, propuesta por John Alan Robinson en 1965 sobre ideas de Martin Davis y Hilary Putnam (1960); es el núcleo de los programas que hoy deciden la satisfacibilidad de fórmulas con millones de variables. A diferencia del sistema de la unidad de deducción, cuyas relaciones con la semántica estudian las clases sobre la corrección y la completitud y sobre el teorema de compacidad, la resolución no deduce conclusiones: refuta conjuntos. Esta clase demuestra que lo hace de modo correcto y completo.

Como en las clases anteriores, $p$, $q$, $r$, $s$ y $t$ nombran las variables $v_1$ a $v_5$; la letra $v$ sin subíndice, y también $w$, designan valoraciones; y $V(\varphi)$ es el conjunto de las variables de $\varphi$.

Cláusulas y conjuntos de cláusulas

Recuérdese de la clase sobre las formas normales que un literal es una variable o la negación de una variable, y que el opuesto de un literal $\ell$, escrito $\ell^{*}$, es el literal de la misma variable y del otro signo; dos literales opuestos forman un par complementario. Por el lema de la negación de un literal, $v(\ell^{*}) = 1 - v(\ell)$ para toda valoración $v$. Allí una cláusula era una disyunción de literales; aquí conviene olvidar el orden y las repeticiones, que no alteran el valor, y quedarse con el conjunto.

Una cláusula es un conjunto finito de literales. La cláusula sin literales se llama cláusula vacía y se escribe $\Box$. Una valoración $v$ satisface una cláusula $C$, y se escribe $v \models C$, si algún literal de $C$ vale $1$ en $v$; en caso contrario, $v$ la refuta. Una cláusula de un solo literal se llama unitaria. Las variables de una cláusula forman el conjunto $V(C)$; las de un conjunto $S$ de cláusulas, el conjunto $V(S)$, unión de los anteriores. Una valoración satisface un conjunto $S$ de cláusulas, $v \models S$, si satisface cada una de sus cláusulas; $S$ es satisfacible si alguna valoración lo satisface, e insatisfacible en caso contrario. Por último, si $S$ es un conjunto de cláusulas y $C$ una cláusula, $S \models C$ significa que toda valoración que satisface $S$ satisface $C$.

Dos casos extremos se siguen de la definición y conviene fijarlos. La cláusula vacía no tiene literales; por tanto, ningún literal suyo vale $1$, y ninguna valoración la satisface: $\Box$ es insatisfacible, y todo conjunto que la contenga también. El conjunto vacío de cláusulas, en cambio, no tiene cláusulas que satisfacer, y toda valoración lo satisface. No deben confundirse: $\{\Box\}$ es insatisfacible y $\emptyset$ es satisfecho por todas las valoraciones.

Una cláusula que contiene un par complementario se llama tautológica: no impone ninguna condición, y puede quitarse de cualquier conjunto sin alterar sus modelos. Escribir las cláusulas como conjuntos no es un capricho de notación. Si de $(p \vee q)$ y $(p \vee \neg q)$ se quiere obtener $p$, la disyunción da $(p \vee p)$, que equivale a $p$ pero no es la misma fórmula; con conjuntos, $\{p\} \cup \{p\} = \{p\}$, y la fusión de los literales repetidos ocurre sola.