¿Cuáles fueron las deficiencias del procedimiento de resolución de Robinson?

Question

Paulson et alii. de LCF a Isabelle / Hol Di:

Resolución para la lógica de primer orden, completa en principio pero con frecuencia decepcionante en la práctica.

Creo que completa significa que pueden probar cualquier fórmula verdadera en la lógica de primer orden correcta.En el Manual de razonamiento automatizado Busco:

La resolución es un método de prueba de teorema completo refutacional: una contradicción (es decir, la cláusula vacía) se puede deducir de cualquier conjunto de cláusulas insatisfactorables.

de Wikipedia:

Intento de probar una fórmula de primer orden satisfactoria que sea insatisfactoria puede resultar en un cálculo de antieminación

¿Por qué es eso decepcionante?

Answer 1

Mientras que "decepcionante en la práctica" ciertamente no es definible formalmente, a diferencia de "completar" (que realmente significa ", eventualmente puede probar todas las fórmulas verdaderas"), es bastante fácil encontrar ejemplos en los que ingenua Ni siquiera es de forma remota adecuada, es decir, los ejemplos que deberían ser fáciles de probar, pero la resolución es extremadamente lenta.

Un ejemplo famoso es una codificación de Principio del agujero de la paloma para $ n $ orificios en la lógica proposicional (que es la declaración " $ n + 1 $ Las palomas no pueden caber en $ n $ orificios sin duplicados). No hay prueba de esta declaración utilizando solo la resolución en el tiempo sub-exponencial en $ n $ .

Las cosas son aún peores en la lógica de predicado, donde es muy fácil encontrar declaraciones sin pruebas de resolución rápida.

Tenga en cuenta que cualquier implementación de la resolución debe implementar una estrategia para elegir las resoluciones, que ya es un problema muy difícil, y un área activa de investigación, ya que la mayoría de los algoritmos prácticos para la demostración del teorema son las mejoras de resolución ingenua, por ejemplo Hyper-resolución .