溯源

“Horn子句”来自于逻辑学家霍恩（Alfred Horn）在1951年发表的文章“On sentences which are true of direct unions of algebras”，首次强调了这种子句的重要性。

Horn子句

在命题逻辑中，Horn子句是带有最多一个肯定变元的子句（文字的析取）。有且只有一个肯定变元的霍恩子句叫做明确子句，只有一个肯定变元的Horn子句叫做事实，没有任何肯定变元的Horn子句叫做目标。

直观的解释

Horn子句表达了什么？

- Horn子句q∨¬p1∨ ... ∨¬pn，表达了规则“如果。。。，那么。。。”，并允许从现有的事实中推导出新的事实。

- Horn子句p，表达了或真或假的原子命题，即事实。例如，“雪是白色的”。

- 否定的Horn子句¬q，表达要实现的目标。事实上，如果我们想证明{H1,...,Hn ⊨ q}，那么q就是求解的目标。现在我们可以通过应用不一致技术的演绎原则，还原为{H1,...,Hn,¬q ⊨∅}，子句¬q是一个否定的Horn子句，模拟目标。

在逻辑编程中的应用

由Horn子句组成的范式是运用已知的归约法（resolution）行之有效的特例。事实上，一组Horn子句的可满足性问题—也被称为HORN-SAT—属于P类，并且对于这个类来说是完整的。因此，Horn子句在逻辑编程中发挥着基本作用。

Prolog编程语言使用的逻辑公式是Horn子句，也就是说，Prolog完全基于Horn子句。上面提到的元素只允许使用命题变量，不允许使用谓词。Prolog在一阶逻辑中运作。因此，有必要将这些结果扩展到谓词计算。

Horn子句的局限性

Horn子句：

- 只有肯定变元可以出现在规则的前提和结论中；

- 只有肯定变元可以作为事实使用。

困境：

- 如何表示否定，以便我们可以表达这样的句子：如果不下雨，我们就去游泳？

解决方案1：将“不下雨”表达为一个明确的命题；

解决方案2：把否定作为失败处理。

然而，这样的解决方案在某种程度上丧失了表达的自然性，。。。

参考文献：

【1】https://fr.wikipedia.org/wiki/Clause_de_Horn

【2】https://blog.sciencenet.cn/home.php?mod=space&uid=2322490&do=blog&id=1367252