Átomo básico
Origem: Wikipédia, a enciclopédia livre.
Considere uma cláusula (disjunção de literais) obtida de uma fórmula sentencial do cálculo de predicados de primeira ordem Φ na forma skolemizada:
então uma expressão atômica obtida a partir de S substituindo todas as variáveis por elementos do Universo de Herbrand H de S é chamada de átomo básico. O conjunto de todos os átomos que podem ser formados a partir de símbolos predicados de S e termos a partir de H é chamado de Base de Herbrand.