霍恩子句
在數理邏輯中,霍恩子句(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.
外部連結
- Alex Sakharov. Horn Clause. MathWorld.