霍恩子句 在数理逻辑中霍恩子句Horn Clause是带有最多一个肯定文字的子句文字的析取霍恩子句得名于逻辑学家 Alfred Horn他在  年首先在文章On sentences which are true of direct unions of algebras Journal of Symbolic Logic   中指出这种子句的重要性 有且只有一个肯定文字的霍恩子句叫做明确子句没有任何肯定文字的霍恩子句叫做目标子句霍恩子句的合取是合取范式也叫做 霍恩公式霍恩子句在逻辑编程中扮演基本角色并且在构造性逻辑中很重要 下面是一个霍恩子句的例子  p   q     t  u displaystyle neg plor neg qvee cdots vee neg tvee u  它可以被等价地写为  p  q    t   u displaystyle pwedge qwedge cdots wedge trightarrow u  霍恩子句对定理证明的实用性是一阶归结提供的两个霍恩子句的归结是一个霍恩子句在自动定理证明中这能导致子句的在计算机上表示得更加高效实际上Prolog 就是完全在霍恩子句上构造的编程语言 霍恩子句在计算复杂性中也是关键的在这里找到一组变量指派使霍恩子句的合取的为真的问题是一个P完全问题有时叫做 HORNSAT这是布尔可满足性问题的 P 的变体它是一个中心的NP完全问题