Un método de prueba que demuestra la insatisfacibilidad de un conjunto de cláusulas aplicando repetidamente la regla de resolución para producir nuevas cláusulas hasta derivar la cláusula vacía, lo que indica una contradicción.

Principio

Usar la regla binaria de resolución para combinar cláusulas que contienen literales complementarios, opcionalmente con unificación en el caso de primer orden, y controlar la búsqueda (selección, ordenación, subsunción) de modo que la derivación de la cláusula vacía sea alcanzable si el conjunto de cláusulas es insatisfacible.

Demostración

Partiendo de las cláusulas {p ∨ q, ¬q ∨ r, ¬r, ¬p}, resolver p ∨ q con ¬p para derivar q, resolver q con ¬q ∨ r para derivar r, resolver r con ¬r para derivar la cláusula vacía, refutando así el conjunto original.

Aplicación incorrecta

Aplicar procedimientos de resolución proposicional sin más a conjuntos de cláusulas del primer orden sin unificación o sin estrategias de terminación, o asumir que la resolución siempre produce pruebas cortas o legibles; la expansión ingenua puede explotar combinatoriamente.

Consecuencia

La refutación por resolución es correcta y, para la lógica proposicional y entornos de primer orden adecuadamente configurados, completa para refutación: si el conjunto de cláusulas es insatisfacible, existe una refutación; sustenta muchos demostradores automáticos y solvers SAT (tras transformación a FNC y a veces con mecanismos adicionales).

Inversión

La inversión es la búsqueda de pruebas constructivas (p. ej. tableau o deducción natural) que produzcan una derivación directa de la fórmula en lugar de refutarla por contradicción; en el enfoque invertido se intenta construir un modelo o prueba directa en vez de derivar una contradicción.

Límite

Aplicable a representaciones en forma de cláusulas (FNC); la resolución pura no construye por sí misma modelos para conjuntos satisfacibles y, en lógica de primer orden, puede no terminar sin estrategias o restricciones adecuadas (p. ej. ordenación, selección o control de bucles).

Tensión semántica

Hay tensión entre la refutación por resolución y estilos de secuencias o deducción natural: la resolución está orientada a la refutación y la búsqueda algorítmica sobre cláusulas, mientras que otros estilos enfatizan la extracción constructiva de testigos y formas de prueba distintas.

Síntesis

La refutación por resolución combina la regla local de resolución con unificación (en primer orden) y control global de búsqueda para derivar contradicciones a partir de conjuntos de cláusulas; transforma la tarea de demostrar validez en una búsqueda sistemática de eliminación de cláusulas que concluye con la cláusula vacía o con la falta de refutación.