Posterior: Algoritmo de Wang Arriba: Procedimientos de demostración automática Anterior: Transformación a forma normal

Transformación a forma normal disyuntiva

Este procedimiento es dual del anterior.

Procedimiento 4.5 (Transformación a FND)  


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. 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 los tuviese $\phi$ y $\phi'$ coinciden Haga $\mbox{\rm FND}(\phi) = \mbox{\rm FND}(\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 ... ...si &\equiv& ( \phi \land \psi) \lor (\neg \phi \lor \neg \psi). \end{eqnarray*}$$
   
   
   
   
   
   En este caso, $\mbox{\rm FND}(\phi) = \mbox{\rm FND}(\phi')$.
3. Si es ``$\lor$'' entonces $\phi$ es de la forma $\phi = \phi_1 \lor \phi_2$. En este caso,
   
   $$\mbox{\rm FND}(\phi)=\mbox{\rm FND}(\phi_1)\cdot \mbox{\rm FND}(\phi_2).$$
   
   

4. Si es ``$\land$'' entonces $\phi$ es de la forma $\phi = \phi_1 \land \phi_2$. En este caso, calcúlese
   
   $$F_1=\mbox{\rm FND}(\phi_1) \mbox{\it y }F_2=\mbox{\rm FND}(\phi_2).$$
   
   
   Concatenemos cada frase en $F_1$ con cada frase en $F_2$. En cada una de las frases obtenidas eliminemos literales repetidas. Sea $F$ la lista que se obtiene de todas esas frases eliminando repeticiones de frases. Tendremos que $\mbox{\rm FND}(\phi)$ es la lista $F$ reducida.
5. Si no hubiera conectivos, entonces $\phi$ ha de ser una variable proposicional $x_i$. En este caso, $\mbox{\rm FND}(\phi)$ es la lista consistente de la única frase cuya única literal es $\phi$ misma. $\bullet$

Posterior: Algoritmo de Wang Arriba: Procedimientos de demostración automática Anterior: Transformación a forma normal