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 α = R ( a , x 2 , f ( x 2 ) , x 4 ) {\displaystyle \alpha \,=R(a,x_{2},f(x_{2}),x_{4})} . O universo de Herbrand para α {\displaystyle \alpha \,} é dado pelo seguinte conjunto:

H α = { a , f ( a ) , f ( f ( a ) ) , f ( f ( f ( a ) ) ) , . . . } {\displaystyle H_{\alpha \,}=\{a,f(a),f(f(a)),f(f(f(a))),...\,\}}

Portanto, a base de Herbrand de α {\displaystyle \alpha \,} é descrita pela seguinte tabela 

     
  
    
      
        
          x
          
            2
          
        
        
      
    
    {\displaystyle x_{2}\,}
  
       
  
    
      
        
          x
          
            4
          
        
        
      
    
    {\displaystyle x_{4}\,}
  
       
  
    
      
        R
        (
        a
        ,
        
          x
          
            2
          
        
        ,
        f
        (
        
          x
          
            2
          
        
        )
        ,
        
          x
          
            4
          
        
        )
        
      
    
    {\displaystyle R(a,x_{2},f(x_{2}),x_{4})\,}
  

     
  
    
      
        a
        
      
    
    {\displaystyle a\,}
  
        
  
    
      
        a
        
      
    
    {\displaystyle a\,}
  
        
  
    
      
        R
        (
        a
        ,
        a
        ,
        f
        (
        a
        )
        ,
        a
        )
        
      
    
    {\displaystyle R(a,a,f(a),a)\,}
  

     
  
    
      
        a
        
      
    
    {\displaystyle a\,}
  
       
  
    
      
        f
        (
        a
        )
        
      
    
    {\displaystyle f(a)\,}
  
      
  
    
      
        R
        (
        a
        ,
        a
        ,
        f
        (
        a
        )
        ,
        f
        (
        a
        )
        )
        
      
    
    {\displaystyle R(a,a,f(a),f(a))\,}
  

    
  
    
      
        f
        (
        a
        )
        
      
    
    {\displaystyle f(a)\,}
  
      
  
    
      
        a
        
      
    
    {\displaystyle a\,}
  
        
  
    
      
        R
        (
        a
        ,
        f
        (
        a
        )
        ,
        f
        (
        f
        (
        a
        )
        )
        ,
        a
        )
        
      
    
    {\displaystyle R(a,f(a),f(f(a)),a)\,}
  

    
  
    
      
        f
        (
        a
        )
        
      
    
    {\displaystyle f(a)\,}
  
     
  
    
      
        f
        (
        a
        )
        
      
    
    {\displaystyle f(a)\,}
  
      
  
    
      
        R
        (
        a
        ,
        f
        (
        a
        )
        ,
        f
        (
        f
        (
        a
        )
        )
        ,
        f
        (
        a
        )
        )
        
      
    
    {\displaystyle R(a,f(a),f(f(a)),f(a))\,}
  

     
  
    
      
        a
        
      
    
    {\displaystyle a\,}
  
      
  
    
      
        f
        (
        f
        (
        a
        )
        )
        
      
    
    {\displaystyle f(f(a))\,}
  
   
  
    
      
        R
        (
        a
        ,
        a
        ,
        f
        (
        a
        )
        ,
        f
        (
        f
        (
        a
        )
        )
        )
        
      
    
    {\displaystyle R(a,a,f(a),f(f(a)))\,}
  

     .        .                  .
     .        .                  .
     .        .                  .

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

Ver também

Referências

  • «Bedregal». , B.R.C, and Acióly, B.M. Lógica para a Ciência da Computação. Versão preliminar, 2002. 
  • «Herbrand Base (MathWorld)» 
  • Portal da matemática