Ground Literal

考慮從 一階邏輯 公式 的 Skolem 正規化 中獲得的子句（字面量的析取）

然後，透過將 的字面量中的所有變數替換為 的 Herbrand 域 的元素而獲得的字面量被稱為 Ground Literal。