Quais foram as falhas de Robinson procedimento de resolução?

Question

Paulson et alii. A partir de LCF Isabelle/HOL dizer:

Resolução para a lógica de primeira ordem, completo, em princípio, mas, freqüentemente, decepcionante na prática.

Eu acho que completa significa que eles podem, à prova de qualquer verdadeira fórmula a lógica de primeira ordem correta.No Manual de Raciocínio Automatizado Eu acho:

A resolução é uma refutationally completa teorema provando método:uma contradição (por exemplo, a cláusula vazia) pode ser deduzida a partir de qualquer unsatisfiable conjunto de cláusulas.

Da Wikipedia:

Para tentar provar uma satisfatível de primeira ordem fórmula como unsatisfiable pode resultar em um nonterminating computação

Por que isso é decepcionante?

Answer 1

Enquanto "decepcionante na prática" certamente não é definível, formalmente, ao contrário de "completo" (que, de fato, significa "pode, eventualmente, provar cada um verdadeiro fórmula"), é muito fácil encontrar exemplos em que ingênua a resolução não está mesmo remotamente adequada, i.é.exemplos que deve ser fácil de provar, mas que resolução é extremamente lento em.

Um exemplo famoso é uma codificação da pigeon hole princípio para $n$ buracos na lógica proposicional (que é a instrução "$n+1$ pombos podem não se enquadrar no $n$ buracos sem duplicatas).Não há nenhuma prova da declaração, utilizando apenas a resolução em tempo sub-exponencial em $n$.

As coisas são ainda piores no predicado lógica, onde é muito fácil encontrar instruções sem qualquer resolução rápida de provas.

Observe que qualquer implementação de resolução deve implementar uma estratégia para escolher o resolvents, o que já é um problema muito difícil, e uma área ativa de pesquisa, pois a maioria dos algoritmos práticos para provando o teorema de são melhorias de ingênua resolução, e.g. o hyper-resolução.