霍恩子句

在数理逻辑中，霍恩子句（Horn Clause）是带有最多一个肯定文字的子句(文字的析取)。霍恩子句得名于逻辑学家 Alfred Horn，他在 1951 年首先在文章《On sentences which are true of direct unions of algebras》, Journal of Symbolic Logic, 16, 14-21 中指出这种子句的重要性。

有且只有一个肯定文字的霍恩子句叫做明确子句，没有任何肯定文字的霍恩子句叫做目标子句。霍恩子句的合取是合取范式，也叫做 霍恩公式。霍恩子句在逻辑编程中扮演基本角色并且在构造性逻辑中很重要。

下面是一个霍恩子句的例子：

$\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$，

它可以被等价地写为：

$(p\wedge q\wedge \cdots \wedge t)\rightarrow u$。

霍恩子句对定理证明的实用性是一阶归结提供的，两个霍恩子句的归结是一个霍恩子句。在自动定理证明中，这能导致子句的在计算机上表示得更加高效。实际上，Prolog 就是完全在霍恩子句上构造的编程语言。

霍恩子句在计算复杂性中也是关键的，在这里找到一组变量指派使霍恩子句的合取的为真的问题是一个P-完全问题，有时叫做 HORNSAT。这是布尔可满足性问题的 P 的变体，它是一个中心的NP-完全问题。

引用

• Alfred Horn, (1951) "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14-21.

外部链接

• Alex Sakharov. Horn Clause. MathWorld. 

本条目部分或全部内容出自以GFDL授权发布的《自由线上电脑词典》（FOLDOC）。