Posterior: Tablas de verdad Arriba: Procedimientos de demostración automática Anterior: Procedimientos de demostración automática

Pruebas por refutación

Observamos que se cumple cada una de las equivalencias lógicas siguientes:

$$\begin{eqnarray*} \phi \rightarrow \psi \mbox{\rm tautolog\'\i a} &\Leftrightar... ...Leftrightarrow& \phi \land \neg \psi \mbox{\rm contradicci\'on} \end{eqnarray*}$$

En consecuencia: $\phi \models \psi \ \Leftrightarrow \ \phi \land {\neg \psi}$ es una contradicción. O, equivalentemente:

$$\{\phi_1,\ldots ,\phi_n\} \models \psi \ \Leftrightarrow \ ... ..._1,\ldots ,\phi_n, \neg \psi\} \mbox{\rm contradicci\'on}.$$ (1)

La equivalencia (1) determina el PRINCIPIO DE PRUEBA POR REFUTACIÓN: Para demostrar $\{\phi_1,\ldots ,\phi_n\} \models \psi$ es suficiente demostrar que $\{\phi_1,\ldots ,\phi_n, \neg \psi\}$ es un conjunto contradictorio de proposiciones. Ahora bien, recordamos que para cada proposición $\phi$ se cumplen las siguientes dos equivalencias:

$$\begin{eqnarray*} \phi &\equiv& \bigvee _{\phi(\mbox{\scriptsize\bf a})=1} \mbo... ...scriptsize\bf a})=0} \mbox{\it Claus}(\overline{\mbox{\bf a}}) \end{eqnarray*}$$

En los métodos de demostración automática que presentaremos en esta sección, consideraremos únicamente el problema de decidir la satisfactibilidad de formas conjuntivas, FC's. Dada una cláusula

$$\mbox{\bf c} = c_1 \lor \ldots \lor c_r \lor c_{r+1} \lor \ldots \lor c_{r+s}$$

reenumeramos a sus componentes, colocando primero las literales que aparezcan negadas. Obtenemos

$$\neg a_1 \lor \ldots \lor \neg a_r \lor b_1 \lor \ldots \lor b_s.$$

Por las Leyes de De Morgan, tendremos

$$\mbox{\bf c} \equiv \neg (a_1 \land \ldots \land a_r) \lor (b_1 \lor \ldots \lor b_s )$$

y como $\neg \phi\lor \psi \equiv \phi\rightarrow \psi$:

$$\mbox{\bf c} \equiv (a_1 \land \ldots \land a_r) \rightarrow (b_1 \lor \ldots \lor b_s ).$$

Con esta notación escribimos:

$$\mbox{\bf c} = [a_1 ,\ldots , a_r ] ; [b_1 ,\ldots , b_s ].$$

Así, una cláusula $\mbox{\bf c} = [ F ; C ]$ se ha de leer como $F \rightarrow C$, donde $F$ es la lista izquierda cuyos elementos están conectados por conjunciones, en tanto que $C$ es la lista derecha cuyos elementos están conectados por disyunciones. En particular:

1. $F = \mbox{\it nil} \ \Rightarrow \ \mbox{\bf c}$ es equivalente a la cláusula $C$.
2. $C = \mbox{\it nil} \ \Rightarrow \ \mbox{\bf c}$ es equivalente a la negación de la frase $F$.

Una proposición $\phi$ escrita en FC queda pues como una lista de cláusulas $\phi = ( [ F_i ; C_i ] )_i.$ Las cláusulas se sobreentienden conectadas por conjunciones. Recordamos que $\mbox{\rm Dos}^n=\{0,1\}^n$ consta de las listas de 0's y 1's de longitud $n$. Éstas representan en binario a los números enteros entre 0 y $2^n- 1$ inclusive. Tal representación es, de hecho, una enumeración de $\mbox{\rm Dos}^n=\{0,1\}^n$. Después de estos preliminares, pasemos a ver diversos algoritmos para decidir cuándo un conjunto dado de proposiciones es o no contradictorio.
Posterior: Tablas de verdad Arriba: Procedimientos de demostración automática Anterior: Procedimientos de demostración automática