Source: http://www.cs.us.es/~fsancho/?e=212
Timestamp: 2019-01-16 11:47:10+00:00

Document:
De la Resolución Proposicional a la Resolución LPO - Fernando Sancho Caparrini
« Metaheurísticas para … « || Inicio || » No me enseñes más pos… »
Última modificación: 22 de Diciembre de 2018, y ha tenido 86 vistas
Nota: Esta entrada no es autocontenida, sino que está orientada a aclarar algunos conceptos de resolución en primer orden a los alumnos del curso de Lógica Informática, por lo que se supone que el lector ha asistido a las clases de esa materia y conoce la nomenclatura usada y los conceptos previos de los que depende.
Breve repaso de la Resolución Proposicional
En el contexto de la Lógica Proposicional, las reglas de producción son mecanismos que permiten obtener nuevas fórmulas. Normalmente, este procedimiento se usa como mecanismo de formación de fórmulas válidas dentro de sistemas deductivos específicos. Ejemplos clásicos de este tipo de reglas serían:
Como generalización de las reglas Modus Ponens, Modus Tollens y Encadenamiento, podemos crear una nueva regla, que denominamos la regla de resolución, para manipular cláusulas de la siguiente forma:
que, formalmente, podemos definir de la siguiente forma: Si \( C_1=\{L_1,\dots,L_n,L\}\) y \(C_2=\{M_1,\dots,M_k,L^c\}\) son dos cláusulas que contienen un literal complementario, entonces la resolvente de ellas respecto de ese literal se define como:
\[C=res_L(C_1,C_2)=\{L_1,\dots,L_n,M_1,\dots,M_k\}\]
Y al igual que ocurre con las reglas anteriores, se puede probar fácilmente que $\{C_1,C_2\}\models C$, por lo que la regla de resolución de convierte en una herramienta adicional para obtener nuevas consecuencias lógicas a partir de un conjunto de cláusulas.
De esta forma, si $\Sigma$ es un conjunto predeterminado de cláusulas, aplicando únicamente la regla de resolución, podemos ir obteniendo otras cláusulas que son deducibles (y por lo que se ha comentado, consecuencias lógicas) de $\Sigma$. Cuando una cláusula $C$ se puede obtener por la aplicación sucesiva de reglas de resolución partiendo de $\Sigma$ lo denotamos por \(\Sigma\vdash_r C\).
De hecho, aunque no es completa, tenemos una relación interesante entre lo que podemos obtener por medio de la aplicación de esta regla y los procedimientos habituales para la consecuencia lógica:
Si \(\Sigma\vdash_r C\) entonces \(\Sigma\models C\). No se tiene la implicación contraria, pero únicamente por el hecho de que la regla de resolución no puede introducir información acerca de literales que no aparecen en las cláusulas originales, algo que sí sucede con la relación de consecuencia lógica general (por ejemplo, $\{p\} \models \{p,q\}$. Sin embargo, si restringimos su uso al proceso de obtención de la cláusula vacía, podemos afirmar algo más interesante:
\(\Sigma\vdash_r \square \Leftrightarrow \Sigma\models \square\), es decir, la regla de resolución es refutacionalmente completa.
Como el problema de consecuencia lógica lo podemos reducir finalmente al problema de satisfactibilidad y consistencia, basta que el sistema sea refutacionalmente completo para que cumpla con nuestras necesidades finales.
De la Resolución Proposicional a la Resolución de Primer Orden
Una vez vista la Resolución Proposicional tenemos una primera forma, rudimentaria y algo ineficiente, de adaptarla a un mecanismo para Lenguajes de Primer Orden: si queremos saber si un conjunto de fórmulas, $\Sigma$, de un LPO es consistente, basta aplicar el Teorema de Herbrand, obtener la extensión de Herbrand de $\Sigma$, $EH(\Sigma)$, y verificar por medio de Resolución Proposicional si $EH(\Sigma)$ es refutable/consistente (trabajando con una forma clausal del mismo) haciendo uso de la regla de resolución proposicional.
Este método tiene el problema de que muy a menudo $EH(\Sigma)$ es un conjunto infinito de cláusulas, por lo que el camino de resolución proposicional se puede hacer altamente ineficiente, ya que generamos muchas cláusulas "proposicionales" que no usamos en el proceso de alcanzar la cláusula vacía (en caso de ser refutable).
Una primera opción, que resulta más económica en consumo de recursos, pasa por generar solo aquellas cláusulas de la extensión de Herbrand que finalmente se usarán para alcanzar la cláusula vacía aunque, sin una estrategia de cómo elegir cuáles serán las cláusulas útiles y con qué asignación de términos cerrados se obtienen, esta opción no asegura encontrar el camino a la solución (y no podemos tener la esperanza de obtener tal estrategia debido a la indecidibilidad de la LPO).
En este caso, decimos que realizamos una resolución restringida (nos restringimos al hecho de sustituir todas las variables libres de las cláusulas iniciales por términos cerrados del lenguaje), por lo que realmente no conseguimos una mejora apreciable respecto al método de resolución proposicional aplicado a la extensión de Herbrand, y puede considerarse que la resolución restringida no es más que una reordenación del método de resolución proposicional (evitando el cálculo previo de todas las fórmulas cerradas, algo que puede ser esencial para que el problema sea abordable).
Una opción más interesante consiste en utilizar un recurso similar pero sin necesidad de llegar a hacer sustituciones de todas las variables libres por términos cerrados. Por ejemplo:
En este caso, decimos que realizamos una resolución no restringida, y permite un mejor aprovechamiento de cálculos intermedios, ahorrando sustituciones completas que pueden simplificarse y reutilizarse si se hacen sustituciones más generales.
Los cambios de variable adecuados pueden simplificar expresiones de dos formas posibles:
Haciendo que varios literales de una misma cláusula se conviertan en un mismo literal.
Haciendo que literales (de distinto signo) de dos cláusulas distintas se conviertan en literales complementarios, con el fin de ser usados para aplicar una resolvente entre ambas cláusulas.
En cualquiera de los dos casos se dice que el cambio de variable unifica los literales que intervienen. Si tal cambio de variable existe, se dice que los literales son unificables, y al cambio de variable se le llama unificador.
En caso de existir, puede ocurrir que el unificador no sea único, sino que haya varios cambios de variable (no esencialmente iguales) que provocan la unificación de la cláusulas en literales distintos. Entre todos estos unificadores hay algunos que son los más generales posibles, en el sentido de que cualquier otro cambio restringe aún más los valores de las variables que aparecen.
Dados dos cambios de variable $\theta$ y $\sigma$, que unifican un conjunto de cláusulas, decimos que $\theta$ es más general que $\sigma$ (para este conjunto de cláusulas) si existe un tercer cambio de variable $\alpha$ de forma que $\sigma=\alpha \circ \theta$.
Es decir, aplicar $\theta$ en vez de $\sigma$ tiene la ventaja de que permite segiur unificando las clásulas, y sin embargo siguen quedando opciones de hacer otros cambios de variable posteriores y reutilizar las cláusulas obtenidas.
Un unificador se dice que es de máxima generalidad (UMG) (para un conjunto de cláusulas unificables) si es más general que cualquier otro unificador posible. Se puede probrar que, en caso de tener un conjunto de cláusulas unificables, siempre existe un UMG para ellas.
Un algoritmo para calcular este UMG consiste en ir identificando los términos que aparecen en las diversas componentes de los literales que se quieren unificar y componer (cuando sea posible) una sustitución que haga que esas identificaciones sean posibles.
Veamos un par de ejemplos de cómo podría funcionar un algoritmo UMG en casos concretos (y de los que podemos extraer el comportamiento general del algoritmo):
Los posibles fallos a los que nos podemos enfrentar en este proceso, y que indicarían que las expresiones no son unificables, serían:
$UMG(P(\cdot),Q(\cdot))$: donde $P$ y $Q$ son predicados distintos.
$UMG(x,f(x))$: donde $f$ es un símbolo de función.
$UMG(f(\cdot),g(\cdot)) $: donde $f$ y $g$ son símbolos de función distintos.
$UMG(t_1,t_2)$: donde $t_1$ y $t_2$ son dos términos cerrados distintos.
$UMG(f(x),t)$: donde $f$ es un símbolo de función y $t$ es un término cerrado (que no comienza por $f$).
Así pues, un objetivo fundamental para la automatización de este procedimiento y mejorar la eficiencia del proceso de resolución para cláusulas de primer orden consiste en saber si dos cláusulas disponibles son unificables, y de qué forma.
Finalmente, consiguiendo los unificadores adecuados, el proceso de resolución no restringida permite obtener cadenas de resoluciones que, generalmente, son más cortas y eficientes que las obtenidas por resoluciones no restringidas, produciendo cláusulas intermedias que son más generales y reutilizables.
En los ejercicios de clase veremos más ejemplos de cómo se pueden resolver problemas de deducción en primer orden usando resolución.

References: Resolución 
 Resolución 
 resolución 
 Resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución