Horn clause（霍恩子句）是数理逻辑与逻辑编程中的一种特殊“子句”（clause）：它在一条析取子句中至多包含一个正文字（positive literal）。在命题逻辑或一阶逻辑里，Horn 子句常被写成“规则”形式，便于推理与自动证明，是 Prolog 等逻辑编程语言的理论基础之一。（注：在更一般的逻辑中还存在非 Horn 子句。）
/ˈhɔːrn klɔːz/
A Horn clause has at most one positive literal.
霍恩子句最多只有一个正文字。
The solver is efficient because the knowledge base is restricted to Horn clauses, which enables fast rule-based inference.
这个求解器之所以高效，是因为知识库被限制为霍恩子句，从而能够进行快速的基于规则的推理。
“Horn clause”中的 Horn 来自美国逻辑学家 Alfred Horn（阿尔弗雷德·霍恩），他在 1951 年研究并系统化了这类子句的性质；clause 在逻辑语境中指“子句/子句式”，即由若干文字构成的公式片段。该术语随后广泛进入自动定理证明、数据库理论与逻辑编程领域。
Select Language