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

Algoritmo de Wang

Procedimiento 4.6 (Algoritmo de Wang)  


Entrada:

Salida:




Algoritmo:

1. Coloque al inicio de $P$ una proposición que no sea una literal.
   1. Sea $\phi$ esta proposición y sea $P'$ el resto de $P$.
   2. Transforme $\phi$ a una proposición equivalente, sólo con conectivos $\lor, \land , \neg$.
   3. Revise el conectivo principal de $\phi$:
      1. Si éste es $\land$, entonces $\phi = \phi_1 \land \phi_2$. Sustituya a $P$ por la lista $[\phi_1, \phi_2] * P'$ (donde $*$ es la concatenación de listas). Invoque a este mismo algoritmo con la sustitución hecha. Si obtiene una respuesta afirmativa $(P,Q)$ es una tautología.
      2. Si éste es $\lor$, entonces $\phi = \phi_1 \lor \phi_2$. Invoque este mismo algoritmo, una vez con el argumento $([\phi_1] * P' , Q)$ y otra con el argumento $([\phi_2] * P' , Q)$. Si en ambos casos obtiene una respuesta afirmativa entonces $(P,Q)$ es una tautología.
      3. Si éste es $\neg$ , entonces $\phi =\neg \phi_1$. Invoque este mismo algoritmo, con el argumento $(P, [\phi_1] * Q)$. Si obtiene una respuesta afirmativa entonces $(P,Q)$ es una tautología.
   4. Si todas las proposiciones en $P$ son literales, considere ahora a $Q$.
2. Coloque al inicio de $Q$ una proposición que no sea una literal.
   1. Sea $\psi$ esta proposición y sea $Q'$ el resto de $Q$.
   2. Transforme $\psi$ a una proposición equivalente, sólo con conectivos $\lor, \land , \neg$.
   3. Revise el conectivo principal de $\psi$.
      1. Si éste es $\lor$, entonces $\psi = \psi_1 \lor \psi_2$. Sustituya a $Q$ por la lista $[\psi_1,\psi_2] * Q'$. Invoque a este mismo algoritmo con la sustitución hecha. Si obtiene una respuesta afirmativa $(P,Q)$ es una tautología.
      2. Si éste es $\land$ , entonces $\psi = \psi_1 \land \psi_2$. Invoque este mismo algoritmo, una vez con el argumento $(P, [\psi_1] * Q')$ y otra con el argumento $(P, [\psi_2] * Q')$. Si en ambos casos obtiene una respuesta afirmativa $(P,Q)$ es una tautología.
      3. Si éste es $\neg$, entonces $\psi = \neg \psi_1$. Invoque este mismo algoritmo, con el argumento $([\psi_1] * P, Q')$. Si obtiene una respuesta afirmativa entonces $(P,Q)$ es una tautología.
   4. Si todas las proposiciones en $Q$ también son literales, continúe con el paso siguiente.
3. Vea si acaso hay una literal común a $P$ y a $Q$.
   1. En este caso $(P,Q)$ es una tautología.
   2. En caso contrario, no lo es, de hecho al hacer a las literales en $P$ verdaderas y a las literales en $Q$ falsas obtenemos una asignación que hace a $(P,Q)$ falsa.
4. En un inicio, si se da una proposición $\phi$, al invocar el algoritmo con el argumento $(\mbox{\it nil},[\phi])$, donde $\mbox{\it nil}$ es la lista vacía, entonces el algoritmo descrito nos dice si $\phi$ es o no una tautología. $\bullet$

De hecho, el algoritmo da más. Por su descripción vemos que gradualmente irá definiendo una estructura arbórea cuyos nodos corresponden a proposiciones. Si al final descartamos a las ``hojas'' que son tautologías, la conjunción de las que nos queden será una FC equivalente a $P \rightarrow Q$.
Posterior: Representación matricial Arriba: Procedimientos de demostración automática Anterior: Transformación a forma normal