Quais foram as deficiências do procedimento de resolução de Robinson?
Paulson et alii. De LCF para Isabelle / HOL diga:
Resolução para lógica de primeira ordem, completa em princípio, mas freqüentemente decepcionante na prática.
Acho que completo significa que eles podem provar qualquer fórmula verdadeira na lógica de primeira ordem correta. No Handbook of Automated Reasoning eu encontro:
Resolução é um método de prova de teorema refutacionalmente completo: uma contradição (isto é, a cláusula vazia) pode ser deduzida de qualquer conjunto insatisfatório de cláusulas.
Da Wikipedia:
Tentar provar uma fórmula de primeira ordem satisfatória como insatisfatória pode resultar em um cálculo não finalizado
Por que isso é decepcionante?
Respostas
Embora "decepcionante na prática" certamente não seja definível formalmente, ao contrário de "completo" (que de fato significa "pode eventualmente provar todas as fórmulas verdadeiras"), é muito fácil encontrar exemplos onde a resolução ingênua não é nem remotamente adequada, ou seja, exemplos que deveriam ser fácil de provar, mas cuja resolução é extremamente lenta.
Um exemplo famoso é uma codificação do princípio da gaveta para$n$ buracos na lógica proposicional (que é a declaração "$n+1$ pombos não cabem $n$furos sem duplicatas). Não há prova desta afirmação usando apenas resolução em tempo subexponencial em$n$.
As coisas são ainda piores na lógica de predicados, onde é muito fácil encontrar declarações sem nenhuma prova de resolução rápida.
Observe que qualquer implementação de resolução deve implementar uma estratégia para escolher os resolventes, que já é um problema muito difícil, e uma área ativa de pesquisa, uma vez que a maioria dos algoritmos práticos para prova de teoremas são aprimoramentos de resolução ingênua, por exemplo, hiper-resolução .