赫布蘭宇宙

考慮一個 一階邏輯 公式 ，採用 Skolem 正規化

那麼 的赫布蘭宇宙 由以下規則定義。

1. 來自 的所有常量都屬於 。如果 中沒有常量，那麼 包含一個任意常量 。

2. 如果 ，並且一個 元函式 出現在 中，那麼 。

透過用赫布蘭宇宙的元素替換 的所有變數而獲得的子句（文字析取）稱為基子句，基文字和基原子也有類似的定義。 可以由來自 的謂詞符號和來自 的項組成的所有基原子的集合稱為赫布蘭基。

赫布蘭宇宙元素的連續生成以及生成元素不可滿足性的驗證可以直接在計算機程式中實現。 鑑於一階邏輯的完備性，該程式基本上是自動化定理證明的工具。 當然，這種窮舉搜尋對於實際應用來說太慢了。

該程式將在所有不可滿足的公式上終止，並且不會在可滿足的公式上終止，這基本上表明不可滿足公式的集合是遞迴可列舉的。 由於一階邏輯中的可證性（或等效地不可滿足性）是遞迴不可判定的，因此該集合不是遞迴的。