Literal básico

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

$\mathrm{\forall }{x}_1...\mathrm{\forall }{x}_{n}S,$

então um literal obtido a partir de $S$ substituindo todas as variáveis por elementos do Universo de Herbrand $H$ de $S$ é chamado literal básico.

Referências

• Predefinição:Citar web

Ver também

• Átomo básico
• Cláusula básica
• Forma normal clausal