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 \Phi na forma skolemizada

         \forall x_{1} ... \forall x_{n}S

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

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

2. Se t_{1} \in H, ... , t_{n} \in H, e uma função n-ária f ocorre em S, então f(t_{1},...,t_{n}) \in H.

As cláusulas (disjunções de literais) obtidas daquelas de S 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 S e termos de H é 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 S= {\neg p(X,Y) \or q(X,f(X)), \neg p(X,Y) \or q(X,g(Y))}

Desde que não existe constante em S, seja então H_{0} = {a}. Assim

H_{1} = H_{0} \cup \{ f(a),g(a) \}
H_{2} = H_{1} \cup \{ f(f(a)),f(g(a)),g(f(a)),g(g(a)) \}
H_{3} = H_{2} \cup \{ f(f(f(a))), f(f(g(a))), f(g(f(a))), f(g(g(a))), g(f(f(a))), g(f(g(a))),
            g(g(f(a))), g(g(g(a))) \}
......
H_{\infty} = \{ a, f(a), g(a), f(f(a)), f(g(a)), g(f(a)), g(g(a)), f(f(f(a))), f(f(g(a))), f(g(f(a))),
        f(g(g(a))), g(f(f(a))), g(f(g(a))), g(g(f(a))), g(g(g(a))), ... \}

2. Seja  S = \{ p(X) \or q(X), r(Z), \neg s(Y) \or t(W) \}

Desde que não exista constante em S, seja então H_{0} = {a}.

Desde que não exista símbolo funcional em S, H_{0} = H_{1} = H_{2} = ... = {a}

Ver também[editar | editar código-fonte]

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