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 um literal obtido a partir de substituindo todas as variáveis por elementos do Universo de Herbrand de é chamado literal básico.
Referências
Ver também Átomo básico Cláusula básica Forma normal clausal
Categoria:Lógica matemática