stringtranslate.com

Resolución (lógica)

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:

dónde

todos , , y son literales,
La línea divisoria significa " implica ".

Lo anterior también puede escribirse como:

O esquemáticamente como:

Tenemos la siguiente terminología:

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).

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 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.

Un ejemplo de este algoritmo es el algoritmo Davis-Putnam original , 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

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.

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]

donde es un unificador más general de y , y y no tienen variables comunes.

Ejemplo

Las cláusulas y pueden aplicar esta regla con como unificador.

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

Aquí vemos que

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:

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). En esta forma, toda cuantificación se vuelve implícita: los cuantificadores universales de las variables ( X , Y , ...) simplemente se omiten como se sobreentiende, mientras que las variables cuantificadas existencialmente se reemplazan por funciones de Skolem .

Por lo tanto,

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

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 ligada, mientras que a es un valor ligado (término). Unificar los dos produce la sustitución

Xa

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:

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]

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 clausular . [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

,

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 tiene 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 

Traugott utiliza la regla

,

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 

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 

Ejemplo de resolución proposicional no clausular

A modo de 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 la comparación de ambas deducciones se desprenden las siguientes cuestiones:

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 ]

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]

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

Véase tambié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. ^ ab 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 la 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).
  8. ^ Wilkins, D. (1973). QUEST: Un sistema de demostración de teoremas no clausulares (Tesis de maestría). Universidad de Essex.
  9. ^ ab 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. ^ abcd 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. ^ abcdef 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. ^ ab 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 .
  15. ^ " " se utiliza para indicar simplificación después de la resolución.
  16. ^ Aquí, " " denota igualdad de términos sintácticos módulo cambio de nombre
  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

Enlaces externos