Resolución (lógica)

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

En lógica matemática y demostración automatizada de teoremas , la resolución es una regla de inferencia que conduce a una técnica de demostración de teoremas con 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 fórmulas, resolviendo el (complemento del) problema booleano de satisfacibilidad . 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 permitió instanciar la fórmula durante la prueba "bajo demanda" tanto como fuera necesario para mantener la integridad 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 complementos si uno es la negación del otro (en lo sucesivo, se considera 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 significa " entraña ".

Lo anterior también se puede escribir 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 |}$

Contamos con 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 producida por la regla de resolución se denomina resolutiva de las dos cláusulas de entrada. Es el principio de consenso aplicado a cláusulas más que a términos. ^[3]

Cuando las dos cláusulas contengan más de un par de literales complementarios, la regla de resolución podrá aplicarse (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 de un literal y de una cláusula de dos literales).

${\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 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 en la base de conocimientos y la negación de la oración a probar (la conjetura ) están conectadas conjuntivamente.
• La oración resultante se transforma en una forma conjuntiva normal, considerando los conjuntos 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 posibles pares de cláusulas que contengan literales complementarios. Después de cada aplicación de la regla de resolución, la frase resultante se simplifica eliminando literales repetidos. Si la cláusula contiene literales complementarios, se descarta (como 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 futuras inferencias de resolución.
• Si después de aplicar una regla de resolución se deriva la cláusula vacía , la fórmula original es insatisfactoria (o contradictoria ), y por tanto se puede concluir que la conjetura inicial se deriva 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 resolutivos.

Esta descripción de la técnica de resolución utiliza un conjunto S como estructura de datos subyacente para representar derivaciones de resolución. Listas , Árboles y Gráficos Acíclicos Dirigidos son otras alternativas posibles y comunes. Las representaciones en árbol son más fieles al hecho de que la regla de resolución es binaria. Junto con una notación posterior para las cláusulas, una representación en árbol también deja claro cómo se relaciona la regla de resolución 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 conjuntos o de listas, porque muestran explícitamente subderivaciones redundantes de cláusulas que se utilizan más de una vez en la derivación de la cláusula vacía. Las representaciones gráficas pueden ser tan compactas en el número de cláusulas como las representaciones de listas y también almacenan información estructural sobre qué cláusulas se resolvieron para derivar cada resolutivo.

Un ejemplo sencillo

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

En lenguaje sencillo: supongamos que es falso. Para que la premisa sea cierta, debe ser cierta. Alternativamente, supongamos que es cierto. Para que la premisa sea cierta, debe ser cierta. 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 para: ^[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 el 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 la inferencia lógica en una sola regla.

Para comprender 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 tanto, Homero es europeo.

O, más generalmente:

${\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 se deben convertir las cláusulas a la forma normal conjuntiva (CNF). De esta forma, toda cuantificación se vuelve implícita: los cuantificadores universales de variables ( X , Y , ...) simplemente se omiten tal como se entiende, 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)}$

Entonces la pregunta es: ¿cómo deriva la técnica de resolución la última cláusula de las dos primeras? La regla es simple:

• Encuentre dos cláusulas que contengan el mismo predicado, donde se niegue en una cláusula pero no en la otra.
• Realizar una unificación sobre los dos predicados. (Si la unificación falla, usted hizo una mala elección de predicados. Vuelva al paso anterior y vuelva a intentarlo).
• Si alguna variable independiente que estaba vinculada en los predicados unificados también aparece en otros predicados en las dos cláusulas, reemplácela allí también con sus valores (términos) vinculados.
• Descarta los predicados unificados y combina 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 ocurre en forma negada

¬P ( X )​

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

P ( una )

en la cláusula segunda. X es una variable independiente, mientras que a es un valor (término) vinculado. La unificación de los dos produce la sustitución.

X ↦ un

Descartar los predicados unificados y aplicar esta sustitución a los predicados restantes (solo Q ( X ), en este caso), produce la conclusión:

Q ( a )

Para otro ejemplo, considere la forma silogística

Todos los cretenses son isleños.

Todos los isleños son unos mentirosos.

Luego todos los cretenses son mentirosos.

O más en general,

∀ X P ( X ) → Q ( X )

∀ X Q ( X ) → R ( X )

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

En CNF, los antecedentes pasan a ser:

¬ P ( X ) ∨ Q ( X )

¬ Q ( Y ) ∨ R ( Y )

(Tenga en cuenta que se cambió el nombre de la variable en la segunda cláusula para dejar claro que las variables en diferentes cláusulas son distintas).

Ahora, 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. Sustituyendo esto en las cláusulas restantes y combinándolas se obtiene la conclusión:

¬ P ( X ) ∨ R ( X )

Factorización

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

Un ejemplo de un conjunto de cláusulas insatisfactorias para el cual se necesita factorización 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}}}$

Dado que cada cláusula consta de dos literales, también lo hace cada posible resolutivo. Por lo tanto, por resolución sin factorización nunca se podrá obtener la cláusula vacía. Usando 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 clausal

Se han ideado generalizaciones de la regla de resolución anterior que no requieren que las fórmulas originales estén en forma clausal normal . ^{[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 forma de cláusula, ^{[10] : 98} y, a veces, ahorran pasos de resolución. ^{[13] : 425}

Resolución no cláusulal 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 una subfórmula y se construye reemplazando en cada aparición de por ; de igual manera para . Se pretende simplificar el resolutivo utilizando reglas como , etc. Para evitar generar resolutivos triviales inútiles, la regla se aplicará sólo cuando tenga al menos una ocurrencia "negativa" y "positiva" ^[14] en y , respectivamente. Murray ha demostrado que esta regla es completa si se aumenta 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 usa 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. Si bien y se construyen como antes, la fórmula se obtiene reemplazando cada aparición positiva y negativa de in por y , respectivamente. De manera similar al enfoque de Murray, se deben aplicar transformaciones simplificadoras apropiadas al resolutivo. 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 }$

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

Ejemplo de resolución proposicional no cláusulal

Como 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 un resolutivo más claro: compare (5) y (10), que resuelven (1) y (2) en . ${\displaystyle p=c}$
• La regla de Murray introdujo 3 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 al de Murray.
• Debido a esta última cuestión, la regla de Traugott puede aprovechar la implicación del supuesto (4), utilizando como fórmula no atómica en el paso (12). Usando las reglas de Murray, la fórmula semánticamente equivalente se obtuvo como (7), sin embargo, no pudo usarse 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 cláusulal 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 es necesario aplicar dichas reglas para lograr su integridad. ^{[ cita necesaria ]} ${\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 común más general, digamos . El resolutivo generalizado se obtiene después de aplicar las fórmulas principales, haciendo aplicable así la versión proposicional. La prueba de integridad 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 . ^[dieciséis] ${\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 para razonar sobre conjuntos de cláusulas donde el símbolo del predicado es la igualdad. Genera todas las versiones "iguales" de 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
• GKC
• Nutria
• prover9
• SNARK
• PASO
• Vampiro
• Probador en línea de Logictools

Ver también

• Desapego 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, Martín; Putnam, Hilary (1960). "Un procedimiento de cálculo para la teoría de la cuantificación". J. ACM . 7 (3): 201–215. doi : 10.1145/321033.321034 . S2CID  31888376.Aquí: pág. 210, "III. Regla para la eliminación de fórmulas atómicas".
2. Robinson 1965
3. DE Knuth, El arte de la programación informática 4A : algoritmos combinatorios , parte 1, p. 539
4. Leitsch 1997, pág. 11 "Antes de aplicar el método de inferencia en sí, transformamos las fórmulas a la forma normal conjuntiva sin 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. pag. 350.ISBN​ 978-0-13-604259-4.
7. Duffy, David A. (1991). Principios de la demostración automatizada de teoremas . Wiley. ISBN 978-0-471-92784-6.Ver pág. 77. El ejemplo aquí se modifica 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 unificabilidad de (5) y (6), necesaria para (7). ${\displaystyle w'}$
8. Wilkins, D. (1973). QUEST: Un sistema de demostración de teoremas no cláusulas (tesis de maestría). Universidad de Essex.
9. Murray, Neil V. (febrero de 1979). Un procedimiento de prueba para una lógica de primer orden no clausal sin cuantificadores (informe técnico). Ingeniería Eléctrica e Informática, Universidad de Syracuse. 39.(Citado de Manna, Waldinger, 1980 como: "Un procedimiento de prueba para la lógica de primer orden no cláusula", 1978)
10. Maná, Zohar ; Waldinger, Richard (enero de 1980). "Un enfoque deductivo de la síntesis de programas". Transacciones ACM sobre lenguajes y sistemas de programación . 2 : 90–121. doi :10.1145/357084.357090. S2CID  14770735.
11. Murray, Nevada (1982). "Demostración de teoremas completamente no cláusulas". Inteligencia artificial . 18 : 67–85. doi :10.1016/0004-3702(82)90011-x.
12. Traugott, J. (1986). "Resolución anidada". VIII Congreso Internacional sobre Deducción Automatizada. CADE 1986 . LNCS . vol. 230. Saltador. 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 Informática . 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 encontradas anteriormente . Por ejemplo, ocurre positivo en y en , negativo 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 el cambio de nombre del módulo de igualdad de términos sintácticos ${\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, Alejandro (1997). El cálculo de resolución. Textos de Informática Teórica. Una serie EATCS. Saltador . 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 y fila .
• Lee, Chin-Liang Chang, Richard Char-Tung (1987). Lógica simbólica y demostración de teoremas mecánicos . Prensa académica. ISBN 0-12-170350-9.{{cite book}}: CS1 maint: multiple names: authors list (link)

enlaces externos

• Alex Sajarov. "Principio de resolución". MundoMatemático .
• Alex Sajarov. "Resolución". MundoMatemático .