霍恩子句

在数理逻辑中，霍恩子句（Horn Clause）是带有最多一个肯定文字的子句(文字的析取)。

简介霍恩子句得名于逻辑学家Alfred Horn，他在 1951 年首先在文章《On sentences which are true of direct unions of algebras》, Journal of Symbolic Logic, 16, 14-21 中指出这种子句的重要性。

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

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

它可以被等价地写为：

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

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

合取范式在布尔逻辑中，如果一个公式是子句的合取，那么它是合取范式(CNF)的。作为规范形式，它在自动定理证明中有用。它类似于在电路理论中的规范和之积形式。

所有的文字的合取和所有的文字的析取是 CNF 的，因为可以被分别看作一个文字的子句的合取和一个单一子句的合取。和析取范式(DNF)中一样，在 CNF 公式中可以包含的命题连结词是与、或和非。非算子只能用做文字的一部分，这意味着它只能在命题变量前出现。2

逻辑编程逻辑编程（逻辑程序设计）是种编程典范，它设置答案须匹配的规则来解决问题，而非设置步骤来解决问题。过程是

事实+规则=结果。

不同的方法，可以看Inductive logic programming。

逻辑编程的要点是将正规的逻辑风格带入计算机程序设计之中。数学家和哲学家发现逻辑是有效的理论分析工具。很多问题可以自然地表示成一个理论。说需要解答一个问题，通常与解答一个新的假设是否跟现在的理论无冲突等价。逻辑提供了一个证明问题是真还是假的方法。创建证明的方法是人所皆知的，故逻辑是解答问题的可靠方法。逻辑编程系统则自动化了这个程序。人工智能在逻辑编程的发展中发挥了重要的影响。

猴子和香蕉问题是逻辑编程社群的著名问题。计算机须自行找出令猴子接触香蕉的可行方法，取代程序员指定猴子接触香蕉的路径和方法。

逻辑编程创建了描述一个问题里的世界的逻辑模型。逻辑编程的目标是对它的模型创建新的陈述。世界上知识不断澎涨。传统来说，我们会将一个问题陈述成单一的假设。逻辑编程的程序透过证明这个假设在模型里是否为真来解决问题。1

本词条内容贡献者为:

杨晓红 - 副教授 - 西南大学