Resolución (lógica)
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 completa de teoremas de refutación 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 insatisfacción 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 semi-algoritmo para el problema de insatisfacción de la lógica de primer orden., proporcionando un método más práctico que el que sigue el 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 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" en la medida necesaria para mantener la integridad de la refutación . [2]
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 adelante , se toma como complemento de ). La cláusula resultante contiene todos los literales que no tienen complementos. Formalmente:
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).