導出原理

${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n$が全て個体閉論理式 として，前節まで議論によれば

$${\cal A}_1,{\cal A}_2,\cdots,{\cal A}_n \vdash_H \cal B$$ (5.20)

を示すには

$${\cal A}_1 \land {\cal A}_2 \land \cdots \land{\cal A} _{n-1} \land {\cal A}_n \land \lnot {\cal B}$$ (5.21)

が充足不能であることを示せばよく，この論理式はさらに 同値変形で以下のようなスコーレム標準形に変形できた。

$$(\forall x_1)(\forall x_2) \cdots (\forall x_n) ({\cal R}_1 \land {\cal R}_2 \land \cdots \land {\cal R}_m)$$ (5.22)

ここで， $x_1,x_2,\cdots,x_n$は ${\cal R}_1 \land {\cal R}_2 \land \cdots \land {\cal R}_m$に現れる 全ての自由変数である。 また各${\cal R}_i$は

$${\cal C}^i_1 \lor {\cal C}^i_2 \lor \cdots \lor {\cal C}^i_{k(i)}$$ (5.23)

の形で，これを節と呼ぶ。
さらに，各${\cal C}^i_j$は 論理記号を含まない論理式${\cal P}^i_j$により，${\cal P}^i_j$ または $\lnot {\cal P}^i_j$である。 これをリテラル(literal)と呼ぶ。