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 refutación técnica completa de demostración de teoremas 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 semi-algoritmo para el problema de insatisfacibilidad de la lógica de primer orden., proporcionando un método más práctico que uno siguiendo 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 permitía instanciar la fórmula durante la prueba "a pedido" en la medida necesaria para mantener la refutación completa . [2]
La regla de resolución en lógica proposicional es una sola 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 producida por la regla de resolución se denomina resolutiva de las dos cláusulas de entrada. Es el principio de consenso aplicado a las cláusulas más que 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 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).