查看“︁霍恩子句”︁的源代码

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

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

下面是一个霍恩子句的例子：
:<math>\neg p \lor \neg q \vee \cdots \vee \neg t \vee u</math>，
它可以被等价地写为：
:<math>(p \wedge q \wedge \cdots \wedge t) \rightarrow u</math>。

霍恩子句对定理证明的实用性是[[一阶归结]]提供的，两个霍恩子句的归结是一个霍恩子句。在[[自动定理证明]]中，这能导致子句的在计算机上表示得更加高效。实际上，[[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.

==外部链接==
* {{MathWorld | urlname=HornClause | title=Horn Clause | author=Alex Sakharov}}
{{FOLDOC}}

[[category:计算机逻辑]]