霍恩子句

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

合取範式

在布爾邏輯中，如果一個公式是子句的合取，那么它是合取範式(CNF)的。作為規範形式，它在自動定理證明中有用。它類似於在電路理論中的規範和之積形式。

所有的文字的合取和所有的文字的析取是 CNF 的，因為可以被分別看作一個文字的子句的合取和一個單一子句的合取。和析取範式(DNF)中一樣，在 CNF 公式中可以包含的命題連結詞是與、或和非。非運算元只能用做文字的一部分，這意味著它只能在命題變數前出現。

邏輯編程

邏輯編程（邏輯程式設計）是種編程典範，它設定答案須匹配的規則來解決問題，而非設定步驟來解決問題。過程是

• 事實+規則=結果。

不同的方法，可以看Inductive logic programming。

邏輯編程的要點是將正規的邏輯風格帶入電腦程式設計之中。數學家和哲學家發現邏輯是有效的理論分析工具。很多問題可以自然地表示成一個理論。說需要解答一個問題，通常與解答一個新的假設是否跟現在的理論無衝突等價。邏輯提供了一個證明問題是真還是假的方法。創建證明的方法是人所皆知的，故邏輯是解答問題的可靠方法。邏輯編程系統則自動化了這個程式。人工智慧在邏輯編程的發展中發揮了重要的影響。

猴子和香蕉問題是邏輯編程社群的著名問題。計算機須自行找出令猴子接觸香蕉的可行方法，取代程式設計師指定猴子接觸香蕉的路徑和方法。

邏輯編程創建了描述一個問題里的世界的邏輯模型。邏輯編程的目標是對它的模型創建新的陳述。世界上知識不斷澎漲。傳統來說，我們會將一個問題陳述成單一的假設。邏輯編程的程式透過證明這個假設在模型里是否為真來解決問題。