霍恩子句

數理邏輯中,霍恩子句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
邏輯編程的要點是將正規的邏輯風格帶入電腦程式設計之中。數學家和哲學家發現邏輯是有效的理論分析工具。很多問題可以自然地表示成一個理論。說需要解答一個問題,通常與解答一個新的假設是否跟現在的理論無衝突等價。邏輯提供了一個證明問題是真還是假的方法。創建證明的方法是人所皆知的,故邏輯是解答問題的可靠方法。邏輯編程系統則自動化了這個程式。人工智慧在邏輯編程的發展中發揮了重要的影響。
猴子和香蕉問題是邏輯編程社群的著名問題。計算機須自行找出令猴子接觸香蕉的可行方法,取代程式設計師指定猴子接觸香蕉的路徑和方法。
邏輯編程創建了描述一個問題里的世界的邏輯模型。邏輯編程的目標是對它的模型創建新的陳述。世界上知識不斷澎漲。傳統來說,我們會將一個問題陳述成單一的假設。邏輯編程的程式透過證明這個假設在模型里是否為真來解決問題。

相關詞條

熱門詞條

聯絡我們