Considere uma cláusula (disjunção de literais) obtida de uma fórmula sentencial do cálculo de predicados de primeira ordem ${\displaystyle \Phi }$ na forma skolemizada:

${\displaystyle \forall x_{1}...\forall x_{n}S,}$

então uma expressão atômica obtida a partir de ${\displaystyle S}$ substituindo todas as variáveis por elementos do Universo de Herbrand ${\displaystyle H}$ de ${\displaystyle S}$ é chamada de átomo básico. O conjunto de todos os átomos que podem ser formados a partir de símbolos predicados de ${\displaystyle S}$ e termos a partir de ${\displaystyle H}$ é chamado de base de Herbrand.

• Sakharov, Alex. «Ground atom» (em inglês). MathWorld. Consultado em 1º de junho de 2010 

• Cláusula básica
• Literal básico
• Forma normal clausal

• Portal da matemática