resolution

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 completa por refutación para oraciones en lógica proposicional y de primer orden. Para la lógica proposicional, aplicar sistemáticamente la regla de resolución actúa como un procedimiento de decisión para la insatisfacibilidad de fórmulas, resolviendo el (complemento del) problema de satisfacibilidad booleana. Para la lógica de primer orden, la resolución se puede usar 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 derivado del teorema de completitud de Gödel. La regla de resolución se remonta a Davis y Putnam (1960); sin embargo, su algoritmo requería probar todas las instancias ground 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 "on demand" justo lo necesario para mantener la completitud por refutación. La cláusula producida por una regla de resolución a veces se denomina resolvente. Resolución en lógica proposicional