¿Cuáles fueron las deficiencias del procedimiento de resolución de Robinson?
Paulson y col. De LCF a Isabelle / HOL diga:
Resolución para la lógica de primer orden, completa en principio pero a menudo decepcionante en la práctica.
Creo que completo significa que pueden probar cualquier fórmula verdadera en la lógica de primer orden correcta. En el Manual de razonamiento automatizado encuentro:
La resolución es un método de prueba de teoremas refutadamente completo: una contradicción (es decir, la cláusula vacía) puede deducirse de cualquier conjunto de cláusulas insatisfactorias.
De Wikipedia:
Intentar demostrar que una fórmula de primer orden satisfactoria es insatisfactoria puede resultar en un cálculo no determinante
¿Por qué es eso decepcionante?
Respuestas
Si bien "decepcionante en la práctica" ciertamente no se puede definir formalmente, a diferencia de "completo" (que de hecho significa "eventualmente puede probar todas las fórmulas verdaderas"), es bastante fácil encontrar ejemplos en los que una resolución ingenua no es ni remotamente adecuada, es decir, ejemplos que deberían ser fácil de probar pero cuya resolución es extremadamente lenta.
Un ejemplo famoso es la codificación del principio de casillero para$n$ agujeros en la lógica proposicional (que es el enunciado "$n+1$ las palomas no pueden caber $n$agujeros sin duplicados). No hay prueba de que esta afirmación utilice únicamente una resolución en el tiempo sub-exponencial en$n$.
Las cosas son aún peores en la lógica de predicados, donde es muy fácil encontrar declaraciones sin pruebas de resolución rápida.
Tenga en cuenta que cualquier implementación de resolución debe implementar una estrategia para elegir los solventes, 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 demostrar teoremas son mejoras de resolución ingenua, por ejemplo, hiperresolución .