Cláusula básica

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 cláusula obtida a partir de ${\displaystyle S}$ substituindo todas variáveis por elementos do universo de Herbrand ${\displaystyle H}$ de ${\displaystyle S}$ é chamada de cláusula básica.