Posterior: Transformación a forma normal Arriba: Procedimientos de demostración automática Anterior: Encadenamiento hacia atrás

Decisión de refutabilidad y satisfactibilidad

Procedimiento 4.3 (Decidir satisfactibilidad)  


Entrada:

Salida:




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

1. 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 ... ... &\equiv& (\neg \phi \lor \psi) \land (\phi \lor \neg \psi). \end{eqnarray*}$$
   
   
   
   
   
   En este caso,
   • $\phi$ es refutable si y sólo si $\phi'$ lo es.
   • $\phi$ es satisfactible si y sólo si $\phi'$ lo es.
2. Si es ``$\lor$'' entonces $\phi$ es de la forma $\phi = \phi_1 \lor \phi_2$. En este caso,
   • $\phi$ es refutable si $\phi_1$ y $\phi_2$ son refutables por sendas asignaciones compatibles entre sí.
   • $\phi$ es satisfactible si cualquiera de $\phi_1$ o $\phi_2$ es satisfactible.
3. Si es ``$\land$'' entonces $\phi$ es de la forma $\phi = \phi_1 \land \phi_2$. En este caso,
   • $\phi$ es refutable si cualquiera de $\phi_1$ o $\phi_2$ es refutable.
   • $\phi$ es satisfactible si $\phi_1$ y $\phi_2$ son satisfactibles por sendas asignaciones compatibles entre sí.
4. Si es ``$\neg$'', entonces $\phi$ es de la forma $\phi =\neg \phi_1$. En este caso,
   • $\phi$ es refutable si $\phi_1$ es satisfactible,
   • $\phi$ es satisfactible si $\phi_1$ es refutable.
5. Si no hubiera conectivos, entonces $\phi$ ha de ser una variable proposicional $\phi_i$. En este caso, $\phi$ es a la vez refutable y satisfactible. $\bullet$

Posterior: Transformación a forma normal Arriba: Procedimientos de demostración automática Anterior: Encadenamiento hacia atrás