Abrir menu principal
Text document with red question mark.svg
Este artigo ou secção contém fontes no fim do texto, mas que não são citadas no corpo do artigo, o que compromete a confiabilidade das informações. (desde março de 2019)
Por favor, melhore este artigo inserindo fontes no corpo do texto quando necessário.
Wikitext.svg
Esta página ou seção precisa ser wikificada (desde março de 2019).
Por favor ajude a formatar esta página de acordo com as diretrizes estabelecidas.

Na lógica matemática, dada uma linguagem formal com um conjunto de símbolos (símbolos de constantes e símbolos funcionais), o universo de Herbrand define recursivamente o conjunto de todos os termos que podem ser compostos aplicando uma composição funcional a partir de símbolos básicos.

Foi assim denominada em homenagem a Jacques Herbrand.

Dada uma linguagem de primeira ordem L, seu universo de Herbrand é definido pelo conjunto de todas as cláusulas básicas que podem ser construídas a partir dos símbolos de L. Levando em conta a definição de termo básico, podemos observar que os símbolos que aparecem em um universo de Herbrand são funtores e constantes de L.

Considere uma fórmula da lógica de primeira ordem na forma skolemizada

         

Então o universo de Herbrand de é definido pelas seguintes regras.

1. Todas as constantes de pertencem a . Se não existem constantes em , então contém uma constante arbitrária .

2. Se , e uma função -ária ocorre em , então .

As cláusulas (disjunções de literais) obtidas daquelas de substituindo todas as variáveis por elementos do universo de Herbrand são chamadas cláusulas básicas, com definições similares para literais básicos e átomos básicos. O conjunto de todos os átomos básicos que pode ser formados a partir de símbolos predicados de e termos de é chamado de Base de Herbrand.

A geração consecutiva de elementos do universo de Herbrand e a verificação de insatisfatibilidade de elementos gerados podem ser diretamente implementadas em um programa de computador. Tendo em vista a completude da lógica de primeira ordem, esse programa é basicamente uma ferramenta para a demonstração automática de teoremas. Evidentemente, essa busca exaustiva é muito lenta para aplicações práticas.

Esse programa irá terminar a execução para todas as fórmulas insatisfatíveis e não terminará para fórmulas satisfatíveis, que basicamente mostra que o conjunto das fórmulas insatisfatíveis é recursivamente enumerável. Dado que a demonstrabilidade (ou, equivalentemente, a insatisfatibilidade) na lógica de primeira-ordem é recursivamente indecidível, esse conjunto não é recursivo.

ExemploEditar

1. Seja  

Desde que não existe constante em  , seja então  . Assim

 
 
 
             
 
 
         

2. Seja  

Desde que não exista constante em  , seja então  .

Desde que não exista símbolo funcional em  ,  

Ver tambémEditar

ReferênciasEditar