赫布兰宇宙

考虑一个 一阶逻辑 公式 ，采用 Skolem 范式

那么 的赫布兰宇宙 由以下规则定义。

1. 来自 的所有常量都属于 。如果 中没有常量，那么 包含一个任意常量 。

2. 如果 ，并且一个 元函数 出现在 中，那么 。

通过用赫布兰宇宙的元素替换 的所有变量而获得的子句（文字析取）称为基子句，基文字和基原子也有类似的定义。 可以由来自 的谓词符号和来自 的项组成的所有基原子的集合称为赫布兰基。

赫布兰宇宙元素的连续生成以及生成元素不可满足性的验证可以直接在计算机程序中实现。 鉴于一阶逻辑的完备性，该程序基本上是自动化定理证明的工具。 当然，这种穷举搜索对于实际应用来说太慢了。

该程序将在所有不可满足的公式上终止，并且不会在可满足的公式上终止，这基本上表明不可满足公式的集合是递归可枚举的。 由于一阶逻辑中的可证性（或等效地不可满足性）是递归不可判定的，因此该集合不是递归的。