Posterior: Programas Arriba: Procedimientos de demostración automática Anterior: Algoritmo de Davis y

Resolución lineal

Se tiene que las siguientes aseveraciones son siempre verdaderas:

1. $(\phi \lor \psi) \land (\neg \phi \lor \xi) \rightarrow (\psi \lor \xi)$ es una tautología.
2. $\{\phi \lor \psi , \neg \phi \lor \xi\}$ es Consistente $\Rightarrow \ \psi \lor \xi$ es Consistente.
3. Principio de Resolución. $\psi \lor \xi$ es contradicción $\Rightarrow \ \{\phi \lor \psi , \neg \phi \lor \xi\}$ es contradicción

Procedimiento 4.9 (Resolución)  


Entrada:

Salida:




Algoritmo indeterminista:

1. Elija una cláusula $a$ de $\phi$. $a$ se dice ser cabecera. Sea $\psi = \phi$ y $b = a$.
2. En tanto que $b$ no sea la cláusula vacía, nil:
   1. Escoja una cláusula $c$, en $\psi$, que se pueda resolver con $b$.
   2. Sea $d$ el resultado de aplicar la resolución, o sea la resolvente de $c$ y $b$.
   3. Sustituya a $\psi$ por $\psi \cup \{d\}$ y a $b$ por $d$ y repita este ciclo.
3. Si no fuera posible encontrar a la cláusula $c$, dé como resultado el valor Indefinido.
4. Si $b$ toma el valor nil, dé esto como respuesta pues en tal caso $\phi$ es una contradicción. $\bullet$

Sobre este algoritmo, formulamos las siguientes observaciones:

1. Es no-determinista pues la elección de $c$ en el punto 1. no está precisada.
2. Si el algoritmo da como resultado el valor nil, entonces en efecto $\phi$ es insatisfactible.
3. Si el algoritmo da como resultado el valor Indefinido, entonces no necesariamente hemos de tener que $\phi$ es satisfactible. Tan solo podemos concluir que la búsqueda realizada ha fracasado en probar que $P$ es insatisfactible.

Posterior: Programas Arriba: Procedimientos de demostración automática Anterior: Algoritmo de Davis y