Herbrand 定理（赫布兰定理）：一阶逻辑中的重要结果，说明一个（通常是无存在量词的）一阶公式如果不可满足，则可以在其由函数符号与常量构成的赫布兰宇宙（Herbrand universe）中找到一个有限的地实例集合，使得这些地实例在命题逻辑层面就已经推出矛盾（不可满足）。它把一阶逻辑的可满足性问题在一定意义上“降”到对有限个地项实例的检查，是自动定理证明、归结（resolution）等方法的理论基础之一。
（注：该定理有多种表述版本，常见于与斯科伦化、子句形式、归结法配套的叙述中。）
/ˈhɛrbrænd ˈθiːərəm/
Herbrand’s theorem is fundamental in automated theorem proving.
赫布兰定理是自动定理证明中的基础性定理。
By applying skolemization and then using Herbrand’s theorem, we can reduce the problem to checking a finite set of ground instances for propositional unsatisfiability.
通过先做斯科伦化、再应用赫布兰定理，我们可以把问题化简为检查有限个地实例在命题层面是否不可满足。
“Herbrand”来自法国逻辑学家 Jacques Herbrand（雅克·赫布兰）的姓氏；“theorem”意为“定理”。该定理源于20世纪早期数理逻辑研究，核心思想是用由语言自身符号生成的“地项世界”（赫布兰宇宙）来刻画一阶推理/不可满足性的证据，从而为后来的机械化推理提供可操作的框架。
Select Language