在數理邏輯和邏輯編程中，霍恩條款是一個具有特殊規則形式的邏輯公式，使其具有用于邏輯編程、形式化規范和模型理論的有用屬性。霍恩條款是以邏輯學家阿爾弗雷德-霍恩命名的，他在1951年首次指出了其重要性。

霍恩子句是一個最多只有一個正字，即無字的子句（字數的二元連接）。反過來說，一個最多只有一個被否定的字詞的字詞連接被稱為雙角句。一個正好有一個正字的Horn子句是一個定語從句或嚴格的Horn子句；一個沒有負字的定語從句是一個單元子句，一個沒有變量的單元子句是一個事實；一個沒有正字的Horn子句是一個目標子句。注意，沒有字的空子句（相當于假）是一個目標子句。這三種Horn子句在下面的命題例子中得到說明。一個子句中的所有變量都被隱含地普遍量化了，其范圍是整個子句。因此，舉例來說。

霍恩條款在構造邏輯和計算邏輯中起著基本作用。它們在一階解析的自動定理證明中很重要，因為兩個霍恩子句的解析器本身就是一個霍恩子句，而一個目標子句和一個確定子句的解析器就是一個目標子句。霍恩子句的這些特性可以使證明一個定理的效率更高：目標子句是這個定理的否定句；見上表中的目標子句。直觀地說，如果我們想證明φ，我們假設?φ（目標），并檢查這種假設是否導致矛盾。如果是，那么φ就一定成立。這樣，一個機械證明工具只需要維護一套公式（假設），而不是兩套（假設和（子）目標）。命題霍恩條款在計算復雜性方面也很有意義。尋找真值分配以使命題霍恩條款的結合體為真，這個問題被稱為HORNSAT。這個問題是P完備的，可以在線性時間內解決。請注意，無限制的布爾可滿足性問題是一個NP完備的問題。

霍恩條款也是邏輯編程的基礎，在邏輯編程中，常見的是以暗示的形式寫定語。(p∧q∧...∧t)→u事實上，用定語從句解析目標從句以產生一個新的目標從句是SLD解析推理規則的基礎，在邏輯編程語言Prolog的實現中使用。在邏輯編程中，定語從句表現為一個目標還原過程。例如，上面寫的Horn條款的行為是這樣的程序。以顯示u，顯示p和顯示q以及...和顯示t。為了強調該子句的這種反向使用，它經常被寫成反向形式。在邏輯編程中，計算和查詢的評估是通過把要解決的問題的負數表示為一個目標句來進行的。例如，解決正字詞的存在性量化聯結的問題。?X(p∧q∧...∧t)是通過否定這個問題（否認它有一個解決方案），并以目標句的邏輯等價形式來表示它。解決這個問題相當于導出一個矛盾，這個矛盾由空句（或假句）表示。

問題的解決是目標句中變量的替換，可以從矛盾的證明中提取。以這種方式使用，目標子句類似于關系數據庫中的共軛查詢，而霍恩子句邏輯在計算能力上等同于通用圖靈機。Prolog的符號實際上是模棱兩可的，"目標句"這個詞有時也被模棱兩可地使用。目標子句中的變量可以被理解為普遍的或存在的量化，推導出"假"可以被解釋為推導出一個矛盾，也可以被解釋為推導出一個待解決的問題的成功方案。VanEmden和Kowalski(1976)在邏輯編程的背景下研究了Horn條款的模型理論特性，表明每一組定語D都有一個xxx的最小模型M。一個原子式A在邏輯上被D暗示，當且僅當A在M中為真。由此可見，當且僅當P在M中為真時，由存在量化的正字連詞表示的問題P在邏輯上被D隱含。Horn條款的最小模型語義是邏輯程序穩定模型語義的基礎。