數理邏輯中,霍恩子句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-完全問題。

引用

編輯
  • Alfred Horn, (1951) "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14-21.

外部連結

編輯

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