Herbrand Universe

释义 Definition

Herbrand Universe（赫布兰宇宙）：在一阶逻辑中，由某个语言/签名（signature）里的常量符号与函数符号递归地构造出的所有无变量（ground）的项（terms）所组成的集合。它常用于赫布兰定理（Herbrand’s theorem）、自动定理证明与逻辑程序（如 Horn 子句/Prolog）的语义与可满足性分析。
（注：在某些表述中，若语言里没有常量，会引入一个“虚拟常量”以保证该集合非空。）

发音 Pronunciation (IPA)

/ˈhɛrbrænd ˈjuːnɪvɝːs/

例句 Examples

Compute the Herbrand universe for this set of function symbols and constants.
计算这组函数符号与常量的 Herbrand universe（赫布兰宇宙）。

By enumerating the Herbrand universe and generating ground instances, the prover applies Herbrand’s theorem to search for a contradiction.
通过枚举赫布兰宇宙并生成无变量实例，证明器利用赫布兰定理来寻找矛盾。

词源 Etymology

Herbrand 来自法国数学家与逻辑学家 Jacques Herbrand（雅克·赫布兰） 的姓氏，该概念与其在证明论与一阶逻辑中的重要结果相关；universe 源自拉丁语 universum（“整体、万物”），在逻辑里借指“讨论对象的总体”，此处特指“由符号可构造出的所有无变量项的总体”。

相关词 Related Words

• Herbrand Base
• Herbrand Interpretation
• Herbrand Theorem
• First-Order Logic
• Ground Term
• Signature
• Skolemization
• Resolution
• Model Theory
• Horn Clause

文学/著作中的用例 Literary Works

• Jacques Herbrand, **Recherches sur la théorie de la démonstration**（1930）：提出并奠定了相关理论背景（常讨论赫布兰定理及其构造思想）。
• Melvin Fitting, **First-Order Logic and Automated Theorem Proving**：在自动定理证明章节中系统使用 Herbrand universe 与 Herbrand base。
• Alan Robinson & Andrei Voronkov (eds.), **Handbook of Automated Reasoning**：在归结（resolution）与可满足性相关章节中频繁出现该术语。