霍恩子句

在數理邏輯中，霍恩子句（Horn Clause）是帶有最多一個肯定文字的子句(文字的析取)。霍恩子句得名於邏輯學家 Alfred Horn，他在 1951 年首先在文章《On sentences which are true of direct unions of algebras》, Journal of Symbolic Logic, 16, 14-21 中指出這種子句的重要性。

有且只有一個肯定文字的霍恩子句叫做明確子句，沒有任何肯定文字的霍恩子句叫做目標子句。霍恩子句的合取是合取範式，也叫做 霍恩公式。霍恩子句在邏輯編程中扮演基本角色並且在構造性邏輯中很重要。

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

$\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$，

它可以被等價地寫為：

$(p\wedge q\wedge \cdots \wedge t)\rightarrow u$。

霍恩子句對定理證明的實用性是一階歸結提供的，兩個霍恩子句的歸結是一個霍恩子句。在自動定理證明中，這能導致子句的在計算機上表示得更加高效。實際上，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.

外部連結

• Alex Sakharov. Horn Clause. MathWorld. 

本條目部分或全部內容出自以GFDL授權發佈的《自由線上電腦詞典》（FOLDOC）。