Posterior: Transformación a forma normal Arriba: Procedimientos de demostración automática Anterior: Decisión de refutabilidad y

Transformación a forma normal conjuntiva

Procedimiento 4.4 (Transformación a FC)  


Entrada:

Salida:




Algoritmo: Dada una proposición $\phi$ revise cuál es su conectivo principal.

1. Si es ``$\neg$'', entonces $\phi$ es de la forma $\phi =\neg \phi_1$. En este caso, revise si $\phi_1$ posee conectivos, y si los tuviese, transforme $\phi$ en $\phi'$ según las fórmulas
   $$\begin{eqnarray*} \neg \neg \phi &\equiv& \phi \\ \neg(\phi \rightarrow \psi)... ... \\ \neg(\phi \land \psi) &\equiv& \neg \phi \lor \neg \psi . \end{eqnarray*}$$
   
   
   
   
   
   Si no hubiese conectivos en $\phi_1$, $\phi$ y $\phi'$ han de coincidir. Haga $\mbox{\rm FC}(\phi) = \mbox{\rm FC}(\phi')$.
2. Si es `` $\leftrightarrow$'' o ``$\rightarrow$'' transforme $\phi$ a una proposición equivalente $\phi'$ en términos de $\neg , \lor, \land$, según las fórmulas
   $$\begin{eqnarray*} \phi \rightarrow \psi &\equiv& \neg \phi \lor \psi \\ \phi ... ...psi &\equiv& (\neg \phi \lor \psi) \land (\phi \lor \neg \psi). \end{eqnarray*}$$
   
   
   
   
   
   En este caso, $\mbox{\rm FC}(\phi) = \mbox{\rm FC}(\phi').$
3. Si es ``$\lor$'' entonces $\phi$ es de la forma $\phi = \phi_1 \lor \phi_2$. En este caso, calcúlese
   
   $$F_1=\mbox{\rm FC}(\phi_1)\mbox{\it y }F_2=\mbox{\rm FC}(\phi_2).$$
   
   
   Concatenemos cada cláusula en $F_1$ con cada cláusula en $F_2$. En cada una de las cláusulas obtenidas eliminemos literales repetidas. Sea $F$ la lista que se obtiene de todas esas cláusulas eliminando repeticiones de cláusulas. Tendremos que $\mbox{\rm FC}(\phi)$ es la lista $F$ reducida.
4. Si es ``$\land$'' entonces $\phi$ es de la forma $\phi = \phi_1 \land \phi_2$. En este caso,
   
   $$\mbox{\rm FC}(\phi)=\mbox{\rm FC}(\phi_1)\cdot \mbox{\rm FC}(\phi_2),$$
   
   
   donde $\cdot$ representa la yuxtaposición de listas, suprimiendo repeticiones de entradas.
5. Si no hubiera conectivos, entonces $\phi$ ha de ser una variable proposicional $x_i$. En este caso, $\mbox{\rm FC}(\phi)$ es la lista consistente de la única cláusula cuya única literal es $\phi$ misma. $\bullet$

Posterior: Transformación a forma normal Arriba: Procedimientos de demostración automática Anterior: Decisión de refutabilidad y