Algoritmo de Resolución en Inteligencia Artificial

Requisito previo:

Los algoritmos de inferencia basados en el trabajo de resolución utilizan la prueba por contradicción. Para establecer que es $K B \models \alpha$ insatisfactorio, demostramos que $(K B \wedge \neg \alpha)$ es insatisfactorio. Hacemos esto demostrando una contradicción.

$\begin{aligned} &\text { function PL-RESOLUTION }(K B, \alpha) \text { returns } t \text { rue or false } \\ &\text { inputs: } K B, \text { the knowledge base, a sentence in propositional logic } \\ &\qquad \alpha, \text { the query, a sentence in propositional logic } \\ &\text { clauses } \leftarrow \text { the set of clauses in the CNF representation of } K B \wedge \neg \alpha \\ &\text { new } \leftarrow\{\} \\ &\text { loop do } \\ &\text { for each pair of clauses } C_{i}, C_{j} \text { in clauses do } \\ &\text { resolvents } \leftarrow \text { PL-RESOLVE }\left(C_{i}, C_{j}\right) \\ &\text { if resolvents contains the empty clause then return } t \text { rue } \\ &\text { new } \leftarrow \text { new } \cup \text { resolvents } \\ &\text { if new } \subseteq \text { clauses then return false } \\ &\text { clauses } \leftarrow \text { clauses } \cup \text { new } \end{aligned}$

Las ecuaciones anteriores muestran un algoritmo de resolución. Para empezar, $(K B \wedge \neg \alpha)$ se transforma a CNF. A continuación, se aplica la regla de resolución a las cláusulas resultantes. Cada par de literales complementarios se resuelve en una nueva cláusula, que se agrega al conjunto si no existía antes. El procedimiento continúa hasta que cualquiera

no se pueden agregar más cláusulas, en cuyo caso, KB no implica
dos cláusulas se resuelven para producir la cláusula vacía, en cuyo caso implica KB.

Debido a que una disyunción es verdadera solo si al menos una de sus disyunciones es verdadera, la cláusula vacía, una disyunción sin disyunciones, es idéntica a Falso. Otro enfoque para reconocer que una oración vacía es una contradicción es notar que solo aparece cuando se resuelven dos oraciones unitarias complementarias, como $P$ y . $\neg P$

En el universo wumpus, podemos usar la técnica de resolución para resolver una inferencia muy fácil. No hay brisa cuando el agente está en [1,1], por lo que no se pueden formar pozos en las casillas cercanas. $K B=R_{2} \wedge R_{4}=\left(B_{1,1} \Leftrightarrow\left(P_{1,2} \vee P_{2,1}\right)\right) \wedge \neg B_{1,1}$ es la base de conocimiento apropiada, y queremos verificar $\alpha$ cuál es, digamos, $P_{1,2}$ . Las cláusulas presentadas en la figura anterior se obtienen por conversión $(K B \wedge \neg \alpha)$ a CNF. Las cláusulas derivadas de la resolución de parejas en la primera fila se muestran en la segunda fila de la imagen. La cláusula vacía, representada como un pequeño cuadrado, se obtiene cuando $P_{1,2}$ se resuelve con $\neg P_{1,2}$ . La figura anterior ilustra que muchas de las etapas de resolución son innecesarias. Por ejemplo, la frase $B_{1,1} \vee \neg B_{1,1} \vee P_{1,2}$ es idéntica a $\text { True } \vee P_{1,2}$ lo que equivale a $True$ . No es particularmente útil deducir que eso $True$ es cierto. Como resultado, se puede eliminar cualquier frase que contenga dos literales complementarios.