Base de Herbrand

Na lógica matemática, dada uma linguagem com um conjunto do universo de Herbrand, a base de Herbrand é o conjunto de todos os átomos basicos que podem ser formados a partir dos símbolos predicados de uma cláusula na forma Skolemizada S e termos do universo Herbrand H de S.

Uma base de Herbrand para uma linguagem de primeira ordem L pode ser construída a partir do universo de Herbrand de L, aplicando algum predicado de L a cada elemento deste universo. Ela consiste portanto do conjunto de todos os átomos básicos que podem ser construídos usando símbolos de L.

Foi assim denominada em homenagem a Jacques Herbrand.

Exemplo

Seja $\alpha \,=R(a,x_{2},f(x_{2}),x_{4})$ . O universo de Herbrand para $\alpha \,$ é dado pelo seguinte conjunto:

$H_{\alpha \,}=\{a,f(a),f(f(a)),f(f(f(a))),...\,\}$

Portanto, a base de Herbrand de $\alpha \,$ é descrita pela seguinte tabela

      $x_{2}\,$         $x_{4}\,$         $R(a,x_{2},f(x_{2}),x_{4})\,$ 
      $a\,$          $a\,$          $R(a,a,f(a),a)\,$ 
      $a\,$         $f(a)\,$        $R(a,a,f(a),f(a))\,$ 
     $f(a)\,$        $a\,$          $R(a,f(a),f(f(a)),a)\,$ 
     $f(a)\,$       $f(a)\,$        $R(a,f(a),f(f(a)),f(a))\,$ 
      $a\,$        $f(f(a))\,$     $R(a,a,f(a),f(f(a)))\,$ 
     .        .                  .
     .        .                  .
     .        .                  .

onde $x_{2}\,$ e $x_{4}\,$ são substituídos em todas as combinações possíveis pelos termos em $H_{\alpha \,}$ , com cada variável sendo substituídas em todas suas ocorrências pelo mesmo termo.