Interpretação de Herbrand
 | Este artigo não cita fontes confiáveis. (Setembro de 2013) |
Na lógica matemática, uma Interpretação de Herbrand é uma interpretação em que todas as constantes e símbolos de função são atribuídos significados muitos simples. Especificamente, toda constante é interpretada como si mesma, e todo símbolo de função é interpretado como a da função que ela aplica. A interpretação também define símbolos de predicado como denotando um subconjunto da base de Herbrand, efetivamente especificando quais as sentenças atômicas são verdade na interpretação. Isso permite que os símbolos num conjunto de cláusulas devem ser interpretadas de uma forma puramente sintática, separada de qualquer instanciação real.
A importância da interpretação de Herbrand é que, se cada interpretação satisfaz um dado conjunto de cláusulas S então há uma interpretação de Herbrand que satisfaz elas. Além disso, o Teorema de Herbrand diz que se S é insatisfatível então existe um conjunto finito insatisfatível de instâncias básicas do universo de Herbrand definido por S. Desde que este conjunto é finito, a sua insatisfatibilidade pode ser verificada em um tempo finito. Contudo, pode haver um número finito de tais conjuntos para verificar.
É nomeado após Jacques Herbrand
