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 de refutación para oraciones en lógica proposicional y lógica de primer orden . En otras palabras, la aplicación iterativa de la regla de resolución de una manera adecuada permite saber si una fórmula proposicional es satisfactoria y probar que una fórmula de primer orden no lo es. Intentar demostrar que una fórmula de primer orden satisfactoria es insatisfactoria puede resultar en un cálculo no determinante; este problema no ocurre en la lógica proposicional.
La regla de resolución se remonta a Davis y Putnam (1960); [1] sin embargo, su algoritmo requería probar todas las instancias terrestres 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 "a pedido" hasta donde fuera necesario para mantener la refutación completa . [2]
La cláusula producida por una regla de resolución se denomina a veces resolutivo .
Resolución en lógica proposicional
Regla de resolución
La regla de resolución en la 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 siguiente, se toma para ser el complemento de ). La cláusula resultante contiene todos los literales que no tienen complementos. Formalmente:
dónde
- todas , , y son literales,
- la línea divisoria significa " implica ".
Lo anterior también se puede escribir como:
La cláusula producido por la regla de resolución se denomina resolvente 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 contienen más de un par de literales complementarios, la regla de resolución se puede aplicar (independientemente) para cada par; sin embargo, el resultado es siempre una tautología .
Modus ponens puede verse como un caso especial de resolución (de una cláusula de un literal y una cláusula de dos literales).
es equivalente a
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 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 que se va a demostrar (la conjetura ) están conectadas de manera conjuntiva.
- La oración resultante se transforma en una forma normal conjuntiva con los conjuntivos vistos como elementos en un conjunto, S , de cláusulas. [4]
- Por ejemplo, da lugar al conjunto .
- La regla de resolución se aplica a todos los posibles pares 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 tautología). De lo contrario, 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 adicionales.
- 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 lo tanto, se puede concluir que la conjetura inicial se sigue de los axiomas.
- Si, por otro lado, la cláusula vacía no se puede derivar y la regla de resolución no se puede aplicar para derivar más cláusulas nuevas, la conjetura no es un teorema de la base de conocimiento original.
Una instancia de este algoritmo es el algoritmo Davis-Putnam original que luego se refinó en el algoritmo DPLL que eliminó la necesidad de una representación explícita de los solventes.
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 de árboles 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 se relaciona 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 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 simple ejemplo
En lenguaje sencillo: supongamos Es falso. Para la premisa a decir verdad, debe ser verdad. Alternativamente, supongaes verdad. Para la premisa a decir verdad, debe ser verdad. Por lo tanto, independientemente de la falsedad o veracidad de, si ambas premisas son válidas, entonces la conclusión es verdad.
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]
dónde es un unificador más general de y , y y no tienen variables comunes.
Ejemplo
Las cláusulas y puede aplicar esta regla con como unificador.
Aquí x es una variable y b es una constante.
Aquí vemos que
- Las cláusulas y son las premisas de la inferencia
- (el resolutivo de las premisas) es su conclusión.
- El literal es el literal resuelto por la izquierda,
- El literal es el literal correcto resuelto,
- es el átomo o pivote resuelto.
- 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 la lógica de términos :
- Todos los griegos son europeos.
- Homero es griego.
- Por tanto, Homer es europeo.
O, de manera más general:
- Por lo tanto,
Para reformular el razonamiento utilizando la técnica de resolución, primero las cláusulas deben convertirse a la forma normal conjuntiva (CNF). De esta forma, toda cuantificación se vuelve implícita: los cuantificadores universales sobre variables ( X , Y , ...) simplemente se omiten tal como se entienden, mientras que las variables cuantificadas existencialmente son reemplazadas por funciones de Skolem .
- Por lo tanto,
Entonces, la pregunta es, ¿cómo la técnica de resolución deriva la última cláusula de las dos primeras? La regla es simple:
- Busque dos cláusulas que contengan el mismo predicado, donde se niega en una cláusula pero no en la otra.
- Realice una unificación en los dos predicados. (Si la unificación falla, hizo una mala elección de predicados. Vuelva al paso anterior e intente nuevamente).
- Si alguna de las variables no vinculadas que estaban vinculadas en los predicados unificados también ocurre en otros predicados en las dos cláusulas, reemplácelas allí también con sus valores vinculados (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 ocurre en forma negada
- ¬ P ( X )
en la primera cláusula, y en forma no negada
- P ( a )
en la segunda cláusula. X es una variable no vinculada , mientras que a es un valor vinculado (término). Unificar los dos 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), 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 mentirosos.
- Por tanto, todos los cretenses son unos 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 se cambió el nombre de la variable en la segunda cláusula para dejar en 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ándolos da la conclusión:
- ¬ P ( X ) ∨ R ( X )
Factorización
La regla de resolución, según la definición de 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 como se define anteriormente. La regla de inferencia resultante es refutación completa, [6] en el sentido de que un conjunto de cláusulas es insatisfactorio si y solo si existe una derivación de la cláusula vacía usando solo resolución, mejorada por factorización.
Un ejemplo de un conjunto de cláusulas insatisfactorias para el que se necesita factorización para derivar la cláusula vacía es:
Dado que cada cláusula consta de dos literales, también lo hace cada posible resolutivo. Por tanto, mediante resolución sin factorización, nunca se podrá obtener la cláusula vacía. Utilizando factorización, se puede obtener, por ejemplo, de la siguiente manera: [7]
Resolución no clausal
Se han ideado generalizaciones de la regla de resolución anterior que no requieren que las fórmulas originarias estén en forma clausal normal . [8] [9] [10] [11] [12] [13]
Estas técnicas son útiles principalmente en el teorema interactivo que demuestra dónde 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 ya veces ahorran pasos de resolución. [13] : 425
Resolución no clausal en lógica proposicional
Para la lógica proposicional, Murray [9] : 18 y Manna y Waldinger [10] : 98 usan la regla
- ,
dónde denota una fórmula arbitraria, denota una fórmula que contiene como una subfórmula, y se construye reemplazando en cada ocurrencia de por ; igualmente para. El resolutivo está destinado a simplificarse utilizando reglas como , etc. Para evitar generar resoluciones triviales inútiles, la regla se aplicará solo cuando tiene al menos una aparición "negativa" y "positiva" [14] en y , respectivamente. Murray ha demostrado que esta regla está completa si se aumenta con reglas de transformación lógica apropiadas. [10] : 103
Traugott usa la regla
- ,
donde los exponentes de indicar la polaridad de sus ocurrencias. Tiempo y se construyen como antes, la fórmula se obtiene reemplazando cada ocurrencia positiva y negativa de en con y , respectivamente. Similar al enfoque de Murray, las transformaciones simplificadoras apropiadas deben aplicarse al resolutivo. Traugott demostró que su regla era completa, siempre queson los únicos conectivos que se utilizan en las fórmulas. [12] : 398–400
La resolución de Traugott es más fuerte que la de Murray. [12] : 395 Además, no introduce nuevas uniones binarias, evitando así una tendencia a la forma clausal en resolución repetida. Sin embargo, las fórmulas pueden crecer más cuando un pequeño se reemplaza varias veces con una mayor y / o . [12] : 398
Ejemplo de resolución proposicional no clausal
Como ejemplo, partiendo de las suposiciones dadas por el usuario
la regla de Murray se puede utilizar de la siguiente manera para inferir una contradicción: [15]
Para el mismo propósito, la regla de Traugott se puede utilizar de la siguiente manera: [12] : 397
De una comparación de ambas deducciones, se pueden ver los siguientes problemas:
- La regla de Traugott puede producir un resolutivo más agudo: compare (5) y (10), que ambos resuelven (1) y (2) en .
- 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 asemejan más al estilo del usuario que el de Murray.
- Debido al último problema, la regla de Traugott puede aprovechar la implicación del supuesto (4), utilizando como la 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 se pudo utilizar como debido a su forma sintáctica.
Resolución no clausal 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 sólida si una sustitución más especialse utiliza, no se necesitan tales aplicaciones de reglas para lograr la completitud. [ cita requerida ]
La regla de Traugott se generaliza para permitir varias subfórmulas distintas por pares de y de , Mientras tener un unificador más general común, digamos . El resolutivo generalizado se obtiene después de aplicara las fórmulas madre, haciendo así aplicable la versión proposicional. La prueba de integridad de Traugott se basa en la suposición de que se usa esta regla completamente general; [12] : 401 no está claro si su regla permanecería completa si se limitara a y . [dieciséis]
Paramodulación
La paramodulación es una técnica relacionada para razonar sobre conjuntos de cláusulas donde el símbolo de 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 en con un subtermo que se unifica con un lado de la igualdad. El subtermo es luego reemplazado 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
- CARINE
- GKC
- Nutria
- Prover9
- SNARK
- SPASS
- Vampiro
Ver 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
- ^ Martin Davis, Hilary Putnam (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 .Aquí: p. 210, "III. Regla para eliminar fórmulas atómicas".
- ^ JA Robinson (enero de 1965). "Una lógica orientada a la máquina basada en el principio de resolución". Revista de la ACM . 12 (1): 23–41. doi : 10.1145 / 321250.321253 .
- ^ DE Knuth, El arte de la programación informática 4A : Algoritmos combinatorios , parte 1, p. 539
- ^ a b Leitsch, Alexander (1997), El cálculo de resolución , EATCS Monographs in Theoretical Computer Science, Springer, p. 11.
Antes de aplicar el método de inferencia en sí, transformamos las fórmulas a la forma normal conjuntiva libre de cuantificadores.
- ^ Enrique P. Arís, Juan L. González y Fernando M. Rubio, Lógica Computacional, Thomson, (2005).
- ^ Stuart J. Russell; Peter Norvig (2009). Inteligencia artificial: un enfoque moderno (3ª ed.). Prentice Hall.pag. 350 (= p. 286 en la 1a edición de 1995)
- ^ David A. Duffy (1991). Principios de la demostración automatizada de teoremas . Nueva York: Wiley.Ver pág. 77. El ejemplo aquí está ligeramente modificado 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), la nueva variable se introdujo para permitir la unificación de (5) y (6), necesaria para (7).
- ^ D. Wilkins (1973). QUEST - Un sistema de prueba de teoremas no clausales (tesis de maestría). Univ. de Essex, Inglaterra.
- ^ a b Neil V. Murray (febrero de 1979). Un procedimiento de prueba para la lógica de primer orden no clausal libre de cuantificadores (informe técnico). Univ. De Syracuse 2-79. (Citado de Manna, Waldinger, 1980 como: "Un procedimiento de prueba para la lógica de primer orden no clausal", 1978)
- ^ a b c d Zohar Manna , Richard Waldinger (enero de 1980). "Un enfoque deductivo de la síntesis del programa" . Transacciones ACM sobre lenguajes y sistemas de programación . 2 : 90-121. doi : 10.1145 / 357084.357090 .Una preimpresión apareció en diciembre de 1978 como Nota técnica 177 del SRI.
- ^ NV Murray (1982). "Demostración del teorema completamente no clausal". Inteligencia artificial . 18 : 67–85. doi : 10.1016 / 0004-3702 (82) 90011-x .
- ^ a b c d e f J. Traugott (1986). "Resolución anidada". Proc. VIII Jornadas de Deducción Automatizada . LNCS . 230 . Saltador. págs. 394–403.
- ^ a b Schmerl, UR (1988). "Resolución sobre árboles de fórmulas". Acta Informatica . 25 : 425–438. doi : 10.1007 / bf02737109 . Resumen
- ^ Estas nociones, llamadas "polaridades", se refieren al número de negaciones explícitas o implícitas encontradas arriba. Por ejemplo, ocurre positivo en y en , negativo en y en , y en ambas polaridades en .
- ^ ""se utiliza para indicar simplificación tras resolución.
- ^ Aquí, ""denota cambio de nombre de módulo de igualdad de términos sintácticos
- ^ Nieuwenhuis, Robert; Rubio, Alberto. "Demostración de teoremas basados en paramodulación". Manual de razonamiento automatizado (PDF) .
Referencias
- Robinson , J. Alan (1965). "Una lógica orientada a la máquina basada en el principio de resolución". Revista de la ACM . 12 (1): 23–41. doi : 10.1145 / 321250.321253 .
- Leitsch, Alexander (1997). El cálculo de resolución . Springer .
- Gallier, Jean H. (1986). Lógica para la informática: fundamentos de la demostración automática de teoremas . Editores de Harper & Row .
- Lee, Chin-Liang Chang, Richard Char-Tung (1987). Demostración de teoremas de lógica simbólica y mecánica ([reimpresión] ed.). San Diego: Prensa académica. ISBN 0-12-170350-9.
enlaces externos
- Alex Sakharov. "Principio de resolución" . MathWorld .
- Alex Sakharov. "Resolución" . MathWorld .