Resolución (lógica)

Regla de inferencia en lógica, teoría de la prueba y demostración automática de teoremas

En lógica matemática y demostración automática de teoremas , la resolución es una regla de inferencia que conduce a una técnica de demostración de teoremas de refutación completa para oraciones en lógica proposicional y lógica de primer orden . Para la lógica proposicional, la aplicación sistemática de la regla de resolución actúa como un procedimiento de decisión para la insatisfacibilidad de la fórmula, resolviendo el (complemento del) problema de satisfacibilidad booleano . Para la lógica de primer orden , la resolución se puede utilizar como base para un semialgoritmo para el problema de insatisfacibilidad de la lógica de primer orden , proporcionando un método más práctico que uno que se deriva del teorema de completitud de Gödel .

La regla de resolución se remonta a Davis y Putnam (1960); ^[1] sin embargo, su algoritmo requería probar todas las instancias básicas de la fórmula dada. Esta fuente de explosión combinatoria fue eliminada en 1965 por el algoritmo de unificación sintáctica de John Alan Robinson , que permitía instanciar la fórmula durante la prueba "a pedido" en la medida necesaria para mantener la completitud de la refutación . ^[2]

La cláusula producida por una regla de resolución a veces se denomina resolutiva .

Resolución en lógica proposicional

Regla de resolución

La regla de resolución en lógica proposicional es una única regla de inferencia válida que produce una nueva cláusula implícita en dos cláusulas que contienen literales complementarios. Un literal es una variable proposicional o la negación de una variable proposicional. Se dice que dos literales son complementarios si uno es la negación del otro (en lo sucesivo, se considera que es el complemento de ). La cláusula resultante contiene todos los literales que no tienen complementos. Formalmente: ${\displaystyle \lnot c}$ ${\displaystyle c}$

${\displaystyle {\frac {a_{1}\lor a_{2}\lor \cdots \lor c,\quad b_{1}\lor b_{2}\lor \cdots \lor \neg c}{a_{1}\lor a_{2}\lor \cdots \lor b_{1}\lor b_{2}\lor \cdots }}}$

dónde

todos , , y son literales, ${\displaystyle a_{i}}$ ${\displaystyle b_{i}}$ ${\displaystyle c}$

La línea divisoria representa " implica ".

Lo anterior también puede escribirse como:

${\displaystyle {\frac {(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow c,\quad c\rightarrow (b_{1}\lor b_{2}\lor \cdots )}{(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow (b_{1}\lor b_{2}\lor \cdots )}}}$

O esquemáticamente como:

${\displaystyle {\frac {\Gamma _{1}\cup \left\{\ell \right\}\,\,\,\,\Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}{\Gamma _{1}\cup \Gamma _{2}}}|\ell |}$

Tenemos la siguiente terminología:

• Las cláusulas y son las premisas de la inferencia. ${\displaystyle \Gamma _{1}\cup \left\{\ell \right\}}$ ${\displaystyle \Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}$
• ${\displaystyle \Gamma _{1}\cup \Gamma _{2}}$(el resolutivo de las premisas) es su conclusión.
• El literal es el literal resuelto a la izquierda, ${\displaystyle \ell }$
• El literal es el literal resuelto correctamente, ${\displaystyle {\overline {\ell }}}$
• ${\displaystyle |\ell |}$es el átomo resuelto o pivote.

La cláusula resultante de la regla de resolución se denomina resolutoria de las dos cláusulas de entrada. Es el principio de consenso aplicado a las cláusulas en lugar de a los términos. ^[3]

Cuando las dos cláusulas contienen más de un par de literales complementarios, la regla de resolución se puede aplicar (independientemente) para cada uno de esos pares; sin embargo, el resultado es siempre una tautología .

El modus ponens puede verse como un caso especial de resolución (de una cláusula uniliteral y una cláusula biliteral).

${\displaystyle {\frac {p\rightarrow q,\quad p}{q}}}$

es equivalente a

${\displaystyle {\frac {\lnot p\lor q,\quad p}{q}}}$

Una técnica de resolución

Cuando se combina con un algoritmo de búsqueda completo , la regla de resolución produce un algoritmo sólido y completo para decidir la satisfacibilidad de una fórmula proposicional y, por extensión, la validez de una oración bajo un conjunto de axiomas.

Esta técnica de resolución utiliza la prueba por contradicción y se basa en el hecho de que cualquier oración en lógica proposicional puede transformarse en una oración equivalente en forma normal conjuntiva . ^[4] Los pasos son los siguientes.

• Todas las oraciones de la base de conocimientos y la negación de la oración a demostrar (la conjetura ) están conectadas conjuntivamente.
• La oración resultante se transforma en una forma normal conjuntiva con los conjuntivos vistos como elementos de un conjunto, S , de cláusulas. ^[4]
  • Por ejemplo, da lugar al conjunto . ${\displaystyle (A_{1}\lor A_{2})\land (B_{1}\lor B_{2}\lor B_{3})\land (C_{1})}$ ${\displaystyle S=\{A_{1}\lor A_{2},B_{1}\lor B_{2}\lor B_{3},C_{1}\}}$
• La regla de resolución se aplica a todos los pares posibles de cláusulas que contienen literales complementarios. Después de cada aplicación de la regla de resolución, la oración resultante se simplifica eliminando los literales repetidos. Si la cláusula contiene literales complementarios, se descarta (como una tautología). Si no es así, y si aún no está presente en el conjunto de cláusulas S , se agrega a S y se considera para inferencias de resolución posteriores.
• Si después de aplicar una regla de resolución se deriva la cláusula vacía , la fórmula original es insatisfacible (o contradictoria ), y por tanto se puede concluir que la conjetura inicial se sigue de los axiomas.
• Si, por otro lado, no se puede derivar la cláusula vacía y no se puede aplicar la regla de resolución para derivar más cláusulas nuevas, la conjetura no es un teorema de la base de conocimiento original.

Un ejemplo de este algoritmo es el algoritmo original de Davis-Putnam , que luego se perfeccionó hasta convertirse en el algoritmo DPLL , que eliminó la necesidad de una representación explícita de los resolventes.

Esta descripción de la técnica de resolución utiliza un conjunto S como la estructura de datos subyacente para representar derivaciones de resolución. Las listas , los árboles y los gráficos acíclicos dirigidos son otras alternativas posibles y comunes. Las representaciones de árbol son más fieles al hecho de que la regla de resolución es binaria. Junto con una notación secuencial para las cláusulas, una representación de árbol también deja en claro cómo la regla de resolución está relacionada con un caso especial de la regla de corte , restringida a fórmulas de corte atómicas. Sin embargo, las representaciones de árbol no son tan compactas como las representaciones de conjunto o lista, porque muestran explícitamente subderivaciones redundantes de cláusulas que se usan más de una vez en la derivación de la cláusula vacía. Las representaciones de gráfico pueden ser tan compactas en el número de cláusulas como las representaciones de lista y también almacenan información estructural sobre qué cláusulas se resolvieron para derivar cada resolvente.

Un ejemplo sencillo

${\displaystyle {\frac {a\vee b,\quad \neg a\vee c}{b\vee c}}}$

En lenguaje sencillo: Supongamos que es falsa. Para que la premisa sea verdadera, debe ser verdadera. Alternativamente, supongamos que es verdadera. Para que la premisa sea verdadera, debe ser verdadera. Por lo tanto, independientemente de la falsedad o veracidad de , si ambas premisas se cumplen, entonces la conclusión es verdadera. ${\displaystyle a}$ ${\displaystyle a\vee b}$ ${\displaystyle b}$ ${\displaystyle a}$ ${\displaystyle \neg a\vee c}$ ${\displaystyle c}$ ${\displaystyle a}$ ${\displaystyle b\vee c}$

Resolución en lógica de primer orden

La regla de resolución se puede generalizar a la lógica de primer orden a: ^[5]

${\displaystyle {\frac {\Gamma _{1}\cup \left\{L_{1}\right\}\,\,\,\,\Gamma _{2}\cup \left\{L_{2}\right\}}{(\Gamma _{1}\cup \Gamma _{2})\phi }}\phi }$

donde es un unificador más general de y , y y no tienen variables comunes. ${\displaystyle \phi }$ ${\displaystyle L_{1}}$ ${\displaystyle {\overline {L_{2}}}}$ ${\displaystyle \Gamma _{1}}$ ${\displaystyle \Gamma _{2}}$

Ejemplo

Las cláusulas y pueden aplicar esta regla con como unificador. ${\displaystyle P(x),Q(x)}$ ${\displaystyle \neg P(b)}$ ${\displaystyle [b/x]}$

Aquí x es una variable y b es una constante.

${\displaystyle {\frac {P(x),Q(x)\,\,\,\,\neg P(b)}{Q(b)}}[b/x]}$

Aquí vemos que

• Las cláusulas y son las premisas de la inferencia. ${\displaystyle P(x),Q(x)}$ ${\displaystyle \neg P(b)}$
• ${\displaystyle Q(b)}$(el resolutivo de las premisas) es su conclusión.
• El literal es el literal resuelto a la izquierda, ${\displaystyle P(x)}$
• El literal es el literal resuelto correctamente, ${\displaystyle \neg P(b)}$
• ${\displaystyle P}$es el átomo resuelto o pivote.
• ${\displaystyle [b/x]}$es el unificador más general de los literales resueltos.

Explicación informal

En la lógica de primer orden, la resolución condensa los silogismos tradicionales de inferencia lógica en una sola regla.

Para entender cómo funciona la resolución, considere el siguiente ejemplo de silogismo de lógica de términos :

Todos los griegos son europeos.

Homero es griego.

Por lo tanto Homero es europeo.

O, de forma más general:

${\displaystyle \forall x.P(x)\Rightarrow Q(x)}$

${\displaystyle P(a)}$

Por lo tanto, ${\displaystyle Q(a)}$

Para reformular el razonamiento utilizando la técnica de resolución, primero las cláusulas deben convertirse a la forma normal conjuntiva (CNF). En esta forma, toda cuantificación se vuelve implícita: los cuantificadores universales sobre las variables ( X , Y , ...) simplemente se omiten como se sobreentiende, mientras que las variables cuantificadas existencialmente se reemplazan por funciones de Skolem .

${\displaystyle \neg P(x)\vee Q(x)}$

${\displaystyle P(a)}$

Por lo tanto, ${\displaystyle Q(a)}$

La pregunta entonces es, ¿cómo se obtiene la última cláusula a partir de las dos primeras? La regla es simple:

• Encuentre dos cláusulas que contengan el mismo predicado, donde se niega en una cláusula pero no en la otra.
• Realice una unificación de los dos predicados. (Si la unificación falla, es porque eligió mal los predicados. Vuelva al paso anterior e inténtelo nuevamente).
• Si alguna variable no enlazada que estaba enlazada en los predicados unificados también aparece en otros predicados en las dos cláusulas, reemplácelas allí también con sus valores enlazados (términos).
• Descarte los predicados unificados y combine los restantes de las dos cláusulas en una nueva cláusula, también unida por el operador "∨".

Para aplicar esta regla al ejemplo anterior, encontramos que el predicado P aparece en forma negada.

¬ P ( X )

en la primera cláusula, y en forma no negada

P ( un )

En la segunda cláusula, X es una variable no vinculada, mientras que a es un valor (término) vinculado. Al unificar los dos se produce la sustitución

X ↦ a

Descartando los predicados unificados y aplicando esta sustitución a los predicados restantes (solo Q ( X ), en este caso), se llega a la conclusión:

Q ( a )

Para otro ejemplo, considere la forma silogística

Todos los cretenses son isleños.

Todos los isleños son mentirosos.

Por lo tanto todos los cretenses son mentirosos.

O más generalmente,

∀ X P ( X ) → Q ( X )

∀ X Q ( X ) → R ( X )

Por lo tanto, ∀ X P ( X ) → R ( X )

En CNF, los antecedentes se convierten en:

¬ P ( X ) ∨ Q ( X )

¬ Q ( Y ) ∨ R ( Y )

(Tenga en cuenta que la variable en la segunda cláusula fue renombrada para dejar en claro que las variables en diferentes cláusulas son distintas).

Ahora bien, unificar Q ( X ) en la primera cláusula con ¬ Q ( Y ) en la segunda cláusula significa que X e Y se convierten en la misma variable de todos modos. Sustituir esto en las cláusulas restantes y combinarlas da la siguiente conclusión:

¬ P ( X ) ∨ R ( X )

Factorización

La regla de resolución, tal como la definió Robinson, también incorporó la factorización, que unifica dos literales en la misma cláusula, antes o durante la aplicación de la resolución, tal como se definió anteriormente. La regla de inferencia resultante es de refutación completa, ^[6] en el sentido de que un conjunto de cláusulas es insatisfacible si y solo si existe una derivación de la cláusula vacía utilizando solo la resolución, mejorada por la factorización.

Un ejemplo de un conjunto de cláusulas insatisfactorias para el cual se necesita factorizar para derivar la cláusula vacía es:

${\displaystyle {\begin{array}{rlcl}(1):&P(u)&\lor &P(f(u))\\(2):&\lnot P(v)&\lor &P(f(w))\\(3):&\lnot P(x)&\lor &\lnot P(f(x))\\\end{array}}}$

Como cada cláusula consta de dos literales, también lo hace cada posible resolutivo. Por lo tanto, mediante la resolución sin factorización, nunca se puede obtener la cláusula vacía. Utilizando factorización, se puede obtener, por ejemplo, de la siguiente manera: ^[7]

${\displaystyle {\begin{array}{rll}(4):&P(u)\lor P(f(w))&{\text{by resolving (1) and (2), with }}v=f(u)\\(5):&P(f(w))&{\text{by factoring (4), with }}u=f(w)\\(6):&\lnot P(f(f(w')))&{\text{by resolving (5) and (3), with }}w=w',x=f(w')\\(7):&{\text{false}}&{\text{by resolving (5) and (6), with }}w=f(w')\\\end{array}}}$

Resolución no clausular

Se han ideado generalizaciones de la regla de resolución anterior que no requieren que las fórmulas originales estén en forma normal de cláusula . ^{[8] [9] [10] [11] [12] [13]}

Estas técnicas son útiles principalmente en la demostración interactiva de teoremas, donde es importante preservar la legibilidad humana de las fórmulas de resultados intermedios. Además, evitan la explosión combinatoria durante la transformación a la forma de cláusula, ^{[10] : 98} y, a veces, ahorran pasos de resolución. ^{[13] : 425}

Resolución no clausular en lógica proposicional

Para la lógica proposicional, Murray ^{[9] : 18} y Manna y Waldinger ^{[10] : 98} utilizan la regla

${\displaystyle {\begin{array}{c}F[p]\;\;\;\;\;\;\;\;\;\;G[p]\\\hline F[{\textit {true}}]\lor G[{\textit {false}}]\\\end{array}}}$,

donde denota una fórmula arbitraria, denota una fórmula que contiene como subfórmula, y se construye reemplazando en cada ocurrencia de por ; lo mismo para . El resolvente se pretende simplificar utilizando reglas como , etc. Para evitar generar resolventes triviales inútiles, la regla se aplicará solo cuando tenga al menos una ocurrencia "negativa" y "positiva" ^[14] en y , respectivamente. Murray ha demostrado que esta regla es completa si se amplía con reglas de transformación lógica apropiadas. ^{[10] : 103} ${\displaystyle p}$ ${\displaystyle F[p]}$ ${\displaystyle p}$ ${\displaystyle F[{\textit {true}}]}$ ${\displaystyle F[p]}$ ${\displaystyle p}$ ${\displaystyle {\textit {true}}}$ ${\displaystyle G}$ ${\displaystyle F[{\textit {true}}]\lor G[{\textit {false}}]}$ ${\displaystyle q\land {\textit {true}}\implies q}$ ${\displaystyle p}$ ${\displaystyle F}$ ${\displaystyle G}$

Traugott utiliza la regla

${\displaystyle {\begin{array}{c}F[p^{+},p^{-}]\;\;\;\;\;\;\;\;G[p]\\\hline F[G[{\textit {true}}],\lnot G[{\textit {false}}]]\\\end{array}}}$,

donde los exponentes de indican la polaridad de sus ocurrencias. Mientras que y se construyen como antes, la fórmula se obtiene reemplazando cada ocurrencia positiva y negativa de en con y , respectivamente. De manera similar al enfoque de Murray, se deben aplicar transformaciones simplificadoras apropiadas al resolvente. Traugott demostró que su regla es completa, siempre que sean los únicos conectivos utilizados en las fórmulas. ^{[12] : 398–400} ${\displaystyle p}$ ${\displaystyle G[{\textit {true}}]}$ ${\displaystyle G[{\textit {false}}]}$ ${\displaystyle F[G[{\textit {true}}],\lnot G[{\textit {false}}]]}$ ${\displaystyle p}$ ${\displaystyle F}$ ${\displaystyle G[{\textit {true}}]}$ ${\displaystyle G[{\textit {false}}]}$ ${\displaystyle \land ,\lor ,\rightarrow ,\lnot }$

El resolvente de Traugott es más fuerte que el de Murray. ^{[12] : 395} Además, no introduce nuevos conjuntores binarios, evitando así una tendencia hacia la forma clausal en la resolución repetida. Sin embargo, las fórmulas pueden alargarse cuando se reemplaza una pequeña varias veces por una mayor y/o . ^{[12] : 398} ${\displaystyle p}$ ${\displaystyle G[{\textit {true}}]}$ ${\displaystyle G[{\textit {false}}]}$

Ejemplo de resolución proposicional no clausular

A modo de ejemplo, partiendo de las suposiciones dadas por el usuario

${\displaystyle {\begin{array}{rccc}(1):&a&\rightarrow &b\land c\\(2):&c&\rightarrow &d\\(3):&b\land d&\rightarrow &e\\(4):&\lnot (a&\rightarrow &e)\\\end{array}}}$

La regla de Murray se puede utilizar de la siguiente manera para inferir una contradicción: ^[15]

${\displaystyle {\begin{array}{rrclccl}(5):&({\textit {true}}\rightarrow d)&\lor &(a\rightarrow b\land {\textit {false}})&\implies &d\lor \lnot a&{\mbox{from (2) and (1), with }}p=c\\(6):&(b\land {\textit {true}}\rightarrow e)&\lor &({\textit {false}}\lor \lnot a)&\implies &(b\rightarrow e)\lor \lnot a&{\mbox{from (3) and (5), with }}p=d\\(7):&(({\textit {true}}\rightarrow e)\lor \lnot a)&\lor &(a\rightarrow {\textit {false}}\land c)&\implies &e\lor \lnot a\lor \lnot a&{\mbox{from (6) and (1), with }}p=b\\(8):&(e\lor \lnot {\textit {true}}\lor \lnot {\textit {true}})&\lor &\lnot ({\textit {false}}\rightarrow e)&\implies &e&{\mbox{from (7) and (4), with }}p=a\\(9):&\lnot (a\rightarrow {\textit {true}})&\lor &{\textit {false}}&\implies &{\textit {false}}&{\mbox{from (4) and (8), with }}p=e\\\end{array}}}$

Para el mismo propósito, la regla de Traugott se puede utilizar de la siguiente manera: ^{[12] : 397}

${\displaystyle {\begin{array}{rcccl}(10):&a\rightarrow b\land ({\textit {true}}\rightarrow d)&\implies &a\rightarrow b\land d&{\mbox{from (1) and (2), with }}p=c\\(11):&a\rightarrow ({\textit {true}}\rightarrow e)&\implies &a\rightarrow e&{\mbox{from (10) and (3), with }}p=(b\land d)\\(12):&\lnot {\textit {true}}&\implies &{\textit {false}}&{\mbox{from (11) and (4), with }}p=(a\rightarrow e)\\\end{array}}}$

De la comparación de ambas deducciones se desprenden las siguientes cuestiones:

• La regla de Traugott puede producir una resolución más nítida: compare (5) y (10), que resuelven (1) y (2) en . ${\displaystyle p=c}$
• La regla de Murray introdujo tres nuevos símbolos de disyunción: en (5), (6) y (7), mientras que la regla de Traugott no introdujo ningún símbolo nuevo; en este sentido, las fórmulas intermedias de Traugott se parecen más al estilo del usuario que las de Murray.
• Debido a este último problema, la regla de Traugott puede aprovechar la implicación del supuesto (4), utilizando como fórmula no atómica en el paso (12). Utilizando las reglas de Murray, se obtuvo la fórmula semánticamente equivalente como (7), sin embargo, no se pudo utilizar como debido a su forma sintáctica. ${\displaystyle p}$ ${\displaystyle a\rightarrow e}$ ${\displaystyle e\lor \lnot a\lor \lnot a}$ ${\displaystyle p}$

Resolución no clausular en lógica de primer orden

Para la lógica de predicados de primer orden, la regla de Murray se generaliza para permitir subfórmulas distintas, pero unificables, y de y , respectivamente. Si es el unificador más general de y , entonces el resolutivo generalizado es . Si bien la regla sigue siendo válida si se utiliza una sustitución más especial , no se necesitan aplicaciones de esa regla para lograr la completitud. ^{[ cita requerida ]} ${\displaystyle p_{1}}$ ${\displaystyle p_{2}}$ ${\displaystyle F}$ ${\displaystyle G}$ ${\displaystyle \phi }$ ${\displaystyle p_{1}}$ ${\displaystyle p_{2}}$ ${\displaystyle F\phi [{\textit {true}}]\lor G\phi [{\textit {false}}]}$ ${\displaystyle \phi }$

La regla de Traugott se generaliza para permitir varias subfórmulas distintas por pares de y de , siempre que tengan un unificador más general común, digamos . El resolvente generalizado se obtiene después de aplicarlo a las fórmulas originales, lo que hace que la versión proposicional sea aplicable. La prueba de completitud de Traugott se basa en el supuesto de que se utiliza esta regla totalmente general; ^{[12] : 401} no está claro si su regla permanecería completa si se restringiera a y . ^[16] ${\displaystyle p_{1},\ldots ,p_{m}}$ ${\displaystyle F}$ ${\displaystyle p_{m+1},\ldots ,p_{n}}$ ${\displaystyle G}$ ${\displaystyle p_{1},\ldots ,p_{n}}$ ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle p_{1}=\cdots =p_{m}}$ ${\displaystyle p_{m+1}=\cdots =p_{n}}$

Paramodulación

La paramodulación es una técnica relacionada con el razonamiento sobre conjuntos de cláusulas donde el símbolo del predicado es la igualdad. Genera todas las versiones "iguales" de las cláusulas, excepto las identidades reflexivas. La operación de paramodulación toma una cláusula from positiva , que debe contener un literal de igualdad. Luego busca una cláusula into con un subtérmino que se unifique con un lado de la igualdad. Luego, el subtérmino se reemplaza por el otro lado de la igualdad. El objetivo general de la paramodulación es reducir el sistema a átomos, reduciendo el tamaño de los términos al sustituir. ^[17]

Implementaciones

• CARINA
• CGC
• Nutria
• Prover9
• SARCAR
• ESPACIO
• Vampiro
• Probador en línea de Logictools

Véase también

• Desprendimiento condensado  : una versión anterior de la resolución
• Programación lógica inductiva
• Resolución inversa
• Programación lógica
• Método de cuadros analíticos
• Resolución SLD
• Inferencia de resolución

Notas

1. Davis, Martin; Putnam, Hilary (1960). "Un procedimiento computacional para la teoría de la cuantificación". J. ACM . 7 (3): 201–215. doi : 10.1145/321033.321034 . S2CID  31888376.Aquí: p. 210, "III. Regla para eliminar fórmulas atómicas".
2. Robinson 1965
3. DE Knuth, El arte de la programación informática 4A : Algoritmos combinatorios , parte 1, pág. 539
4. Leitsch 1997, p. 11 "Antes de aplicar el método de inferencia en sí, transformamos las fórmulas a una forma normal conjuntiva libre de cuantificadores".
5. Arís, Enrique P.; González, Juan L.; Rubio, Fernando M. (2005). Lógica Computacional. Ediciones Paraninfo, SA ISBN 9788497321822.
6. Russell, Stuart J.; Norvig, Peter (2009). Inteligencia artificial: un enfoque moderno (3.ª ed.). Prentice Hall. pág. 350. ISBN 978-0-13-604259-4.
7. Duffy, David A. (1991). Principios de demostración automática de teoremas . Wiley. ISBN 978-0-471-92784-6.Véase la pág. 77. El ejemplo que se muestra aquí se ha modificado ligeramente para demostrar una sustitución de factorización no trivial. Para mayor claridad, el paso de factorización (5) se muestra por separado. En el paso (6) se introdujo la nueva variable para permitir la unificación de (5) y (6), necesaria para (7). ${\displaystyle w'}$
8. Wilkins, D. (1973). QUEST: Un sistema de demostración de teoremas no clausulares (Tesis de maestría). Universidad de Essex.
9. Murray, Neil V. (febrero de 1979). Un procedimiento de prueba para lógica de primer orden no clausular sin cuantificadores (informe técnico). Ingeniería eléctrica y ciencias de la computación, Universidad de Syracuse. 39.(Citado de Manna, Waldinger, 1980 como: "Un procedimiento de prueba para la lógica de primer orden no clausular", 1978)
10. Manna, Zohar ; Waldinger, Richard (enero de 1980). "Un enfoque deductivo para la síntesis de programas". ACM Transactions on Programming Languages ​​and Systems . 2 : 90–121. doi :10.1145/357084.357090. S2CID  14770735.
11. Murray, NV (1982). "Demostración de teoremas completamente no clausulares". Inteligencia artificial . 18 : 67–85. doi :10.1016/0004-3702(82)90011-x.
12. Traugott, J. (1986). "Resolución anidada". 8.ª Conferencia internacional sobre deducción automatizada. CADE 1986. LNCS . Vol. 230. Springer. págs. 394–403. doi :10.1007/3-540-16780-3_106. ISBN. 978-3-540-39861-5.
13. Schmerl, UR (1988). "Resolución sobre árboles de fórmulas". Acta Informatica . 25 (4): 425–438. doi :10.1007/bf02737109. S2CID  32702782.Resumen
14. Estas nociones, llamadas "polaridades", se refieren al número de negaciones explícitas o implícitas que se encuentran arriba . Por ejemplo, ocurre positiva en y en , negativa en y en , y en ambas polaridades en . ${\displaystyle p}$ ${\displaystyle p}$ ${\displaystyle (p\land q)\lor r}$ ${\displaystyle q\rightarrow p}$ ${\displaystyle \lnot (p\land q)\lor r}$ ${\displaystyle p\rightarrow q}$ ${\displaystyle p\leftrightarrow q}$
15. " " se utiliza para indicar simplificación después de la resolución. ${\displaystyle \implies }$
16. Aquí, " " denota igualdad de términos sintácticos módulo cambio de nombre ${\displaystyle =}$
17. Nieuwenhuis, Robert; Rubio, Alberto (2001). "7. Demostración de teoremas basada en paramodulación" (PDF) . En Robinson, Alan JA; Voronkov, Andrei (eds.). Manual de razonamiento automatizado. Elsevier. págs. 371–444. ISBN. 978-0-08-053279-0.

Referencias

• Robinson , J. Alan (1965). "Una lógica orientada a máquinas basada en el principio de resolución". Revista de la ACM . 12 (1): 23–41. doi : 10.1145/321250.321253 . S2CID  : 14389185.
• Leitsch, Alexander (1997). El cálculo de resolución. Textos de informática teórica. Serie EATCS. ​​Springer . ISBN 978-3-642-60605-2.
• Gallier, Jean H. (1986). Lógica para la informática: fundamentos de la demostración automática de teoremas. Harper & Row .
• Lee, Chin-Liang Chang, Richard Char-Tung (1987). Lógica simbólica y demostración de teoremas mecánicos . Academic Press. ISBN 0-12-170350-9.{{cite book}}: CS1 maint: multiple names: authors list (link)

Enlaces externos

• Alex Sakharov. "Principio de resolución". MathWorld .
• Alex Sakharov. "Resolución". MathWorld .