Universo de Herbrand

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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.

Exemplo[editar | editar código-fonte]

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ém[editar | editar código-fonte]

Referências[editar | editar código-fonte]