霍恩子句

霍恩子句（Horn Clause）是數理邏輯中的一個重要概念，得名於邏輯學家Alfred Horn，他在1951年的文章《On sentences which are true of direct unions of algebras》中首次提出了這種子句的重要性。

霍恩子句的定義是：一個子句（即一組文字的析取）中，要麼有一個肯定文字（即出現在子句中的文字），要麼沒有肯定文字。只有肯定文字的霍恩子句稱為明確子句，而沒有肯定文字的霍恩子句稱為目標子句。霍恩子句的合取是合取範式，也稱為霍恩公式。

霍恩子句在邏輯編程中扮演著基本角色，並且在構造性邏輯中非常重要。例如，Prolog語言就是完全基於霍恩子句構建的。

此外，霍恩子句在計算複雜性理論中也是一個關鍵概念。確定一組變數指派使霍恩子句的合取為真的問題是一個P-完全問題，稱為HORNSAT，它是布爾可滿足性問題的中心NP-完全問題。

總的來說，霍恩子句是對邏輯編程和自動定理證明等領域有重要影響的邏輯概念。