Horn子句
维基百科，自由的百科全书
在逻辑学，特别是命题逻辑中，Horn 子句或明确子句是有如下一般性形式的命题: (p 与 q 与 ... 与 t) 蕴涵 u，这里的由与组合的命题的数目同我们所希望的一样大(也可以是零)。
假如你在常见的经典逻辑下工作，这种形式是可以改写的。逻辑条件经常被表达为一个析取式：下列二者是等价的
- p 蕴涵 u
和
- (非 p) 或 u 。
上面的一般性的 Horn 子句表达式的等价形式也可普遍化为
- (非 p) 或 ... 或 (非 t) 或 u。
换句话说，Horn 子句是一种简单的析取式，在其中最多有一个项是肯定的文字(literal)，而余下的是否定的。这显示了 Horn 子句的合取是合取范式。Horn 子句在逻辑编程中扮演基本角色并且在构造性逻辑中很重要。
Horn 子句对定理证明的实用性是一阶归结提供的，两个 Horn 子句的归结是一个 Horn 子句。在自动定理证明中，这能导致子句的在计算机上表示得更加高效。实际上，Prolog 就是完全在 Horn 子句上构造的编程语言。
Horn 子句在计算复杂性中也是关键的，在这里找到一组变量指派使 Horn 子句的合取的为真的问题是一个P-完全问题，有时叫做 HORNSAT。这是布尔可满足性问题的 P 的变体，它是一个中心的NP-完全问题。
"Horn 子句"得名于逻辑学家 Alfred Horn，他是在 1951 年首次指出这种子句的重要性的人，那是在文章 "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14-21 中。
| 本文參考素材源自「FOLDOC」，在GFDL下授權。 This article was originally based on material from the Free On-line Dictionary of Computing and is used under the GFDL. |
