Átomo básico

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

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

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.

Referências

• Sakharov, Alex. Ground atom (em inglês). MathWorld. Página visitada em 1º de junho de 2010.

Ver também

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