El principio detrás de la resolución es que dados dos disyunciones, decir $p \lor r$$\lnot r \lor q$, en el modelo que satisface a ambas deben también satisfacer la disyunción $p \lor q$, ya que si el modelo satisface $p \lor r$ por virtud de $r$ ser verdad, entonces no puede también hacer $\lnot r \lor q$ verdadera en virtud de $\lnot r$ ser verdad. Del mismo modo, si el modelo es $\lnot r$ verdadera, entonces si hacer $p \lor r$ cierto, debe haber hecho $p$ cierto. Desde cualquiera de las $r$ o $\lnot r$ verdadera, entonces cualquiera de las $p$ o $q$ debe ser verdadera, y por lo tanto $p \lor q$ cierto.
Para la lógica proposicional, un algoritmo de resolución se inicia con un conjunto de cláusulas y elige un par de las cláusulas de $c_1$ $c_2$ que contienen literales complementarios (es decir, uno que contiene algunos proposición $\phi$ y el otro contiene $\lnot \phi$) y que no han sido recogidos. El algoritmo resuelve las cláusulas para formar una nueva cláusula que contiene todos los literales de la a $c_1$ $c_2$ a excepción de $\phi$ $\lnot \phi$ y se añade el nuevo apartado para el conjunto de cláusulas. Cualquier cláusula que contiene un literal y su complemento (es decir, algunos $\phi$$\lnot \phi$) puede ser inmediatamente eliminado el conjunto de cláusulas, como es tautologous. Este proceso continúa hasta que un vacío cláusula se deriva, en cuyo caso el original conjunto de cláusulas es unsatisfiable, o de lo contrario no hay más de resolverse de cláusulas, que indica que el original conjunto de cláusulas es válido.
En el caso de la lī ogica de donde cláusulas contienen sólo tierra literales (es decir, no hay variables), un algoritmo de resolución puede hacer exactamente la misma cosa. Por ejemplo, $\{p(a) \lor q(b)\}$ puede ser resuelto con $\{\lnot q(b) \lor p(b)\}$ rendimiento $\{p(a) \lor p(b)\}$.
Cuando los literales contienen variables, sin embargo, el proceso se vuelve más complicado. Cada variable está implícitamente universalmente cuantificada sobre cada una de las cláusulas, por lo que una cláusula como $\{p(x) \lor q(x)\}$ significa que por cada $x$ ,$p(x) \lor q(x)$. Considere la posibilidad de resolver esa cláusula con, por ejemplo, $\{\lnot p(a)\}$. Ambos contienen un literal en la relación $p$, pero el plazo $a$ es una constante, mientras que $x$ es universalmente cuantificado variable. Podríamos intentar crear una instancia de $\{p(x) \lor q(x)\}$ $a$ rendimiento $\{p(a) \lor q(a)\}$ y, a continuación, resolver este con $\{\lnot p(a)\}$ rendimiento $\{q(a)\}$. De hecho, este es válida, y $\{q(a)\}$ es un resultado que nos gustaría ver. El algoritmo de resolución logra esto por encontrar un unificador para los servicios complementarios de literales (en este caso, $\sigma = [x/a]$), aplicando para ello las dos cláusulas, y unifica como en el de la proposicional caso. Por supuesto, esto significa que no es suficiente simplemente para encontrar un literales $p(\dots)$$\lnot p(\dots)$; resolver las dos cláusulas, el complemento de los literales deben unifiable. Desde hace dos cláusulas pueden utilizar la misma variable, el cambio de nombre de las variables puede ser necesario antes de dos cláusulas puede ser resuelto.
Por lo tanto, echemos un vistazo al problema en cuestión. El conjunto de cláusulas es:
- $\{P(x,y), P(f(y),z), Q(x,y)\}$
- $\{\lnot P(y, a), Q(y, x)\}$
- $\{R(h(x), x), \lnot Q(x, a)\}$
- $\{\lnot R(x, y), \lnot R(h(z), y), \lnot Q(z, u)\}$
Empezamos por la búsqueda de dos cláusulas con unifiable literales complementarios, digamos, 2 y 3, basado en los literales $Q(y,x)$ entre 2 y $\lnot Q(x,a)$ a partir de 3. La variable $x$ aparece en ambos, así que vamos a reescribir 3 de 3 " por la sustitución de $x$ $z$ dar $\{R(h(z), z), \lnot Q(z,a)$. Que se ocupa de la re-etiquetado. Los literales $Q(y,x)$ entre 2 y $Q(z,a)$ a partir de 3 (aviso que nos dejó la negación para el propósito de unificar) están unificadas bajo la sustitución de $\sigma = [y/z, x/a]$. (Para obtener información sobre cómo encontrar el unificador más general, véase, por ejemplo, S. Tanimoto las diapositivas en la unificación.) La aplicación de $\sigma$ a 2 y de 3' da las cláusulas
- $\{\lnot P(z,a), Q(z,a)\}$
- $\{R(h(z),z), \lnot Q(z,a)\}$
que puede resolverse para obtener la nueva cláusula
$$ \{\lnot P(z,a), R(h(z),z) \} $$
Seguir haciendo esto, y, finalmente, la cláusula vacía aparecerá, mostrando que el conjunto inicial es unsatisfiable.
El ejemplo que acabo de utilizar a cabo la resolución en dos cláusulas donde uno literal de cada uno eran complementarias. Es decir, el 2 contiene sólo un literal positivo en $Q$, y 3' sólo contiene un literal negativo en $Q$. Algunas de las resoluciones que en el ejemplo de la pregunta, sin embargo, el uso de más de dos literales. Por ejemplo, en las cláusulas (después de cambiar el nombre)
- $\{P(x,y), P(f(y),z), Q(x,y)\}$
- $\{\lnot P(y_1,a), Q(y_1,x_1)\}$
hay, por $P$, dos literales positivos y uno negativo literal. La mayoría de los generales unificador de estos tres literales es
$$ \sigma = [y/a, z/a, x/f(a), y_1/f(a)] $$
Tanimoto las diapositivas vinculado anteriormente sólo describir cómo encontrar la más general unificador de dos literales, pero hay un montón de recursos que describe multi-literal unificación así, por ejemplo, Kutsia las diapositivas. En realidad es sólo una generalización de los binarios de caso; en lugar de escanear dos literales buscando desajustes, escanear todos los literales. En este caso, el conjunto de literales que contiene
- $P(x,y)$
- $P(f(y),z)$
- $\lnot P(y_1,a)$ (pero durante la exploración, ignoramos la negación)
Caminar a través de todo el algoritmo de unificación es un poco tedioso, pero Kutsia las diapositivas por encima de la cubierta (junto con las sustituciones y la sustitución de la composición) en detalle. Intuitivamente, sin embargo, el segundo de los argumentos a $P$ $y$, $z$, y $a$. Desde $a$ es un no-término variable, tanto en $y$ $z$ debe ser reemplazado por $a$, por lo que esperamos que nuestros sustitución para contener $[y/a, z/a]$. Si esta sustitución es, en efecto, a pesar de que, el primero de los argumentos a $P$ $x$, $f(a)$, y $y_1$. Desde $f(a)$ es un terreno plazo, y tanto $x$ $y_1$ son variables, la sustitución debe también contener $[x/f(a), y_1/f(a)]$. Ahora, el proceso de combinación de las sustituciones (sustitución de composición) puede ser difícil, pero este no es realmente uno de los complicados casos, y el final de la sustitución es sólo $[y/a, z/a, x/f(a), y_1/f(a)]$.
Como un aparte, en otro tipo de recursos en las sustituciones y la unificación, los autores utilizan diferentes convenios para denotar las sustituciones, en particular si $[x/y]$ es la sustitución de un producto que reemplaza$x$$y$, o la sustitución de un producto que reemplaza$y$$x$. Personalmente, soy aficionado a de la $[x/y]$ lo que significa que $y$ será reemplazado con $x$, debido a la sintáctica paralela con la aritmética, donde$(x/y)y$$x$, puesto que el $y$'s "cancelar". Esa es mi preferencia, pero no es universal (como la pregunta original muestra), y ambos están presentes en la literatura.
