ホーン節（ホーンせつ、）とは、数理論理学において、節（リテラルの選言結合命題）のうち、肯定形のリテラルの数が1つ以下の物を言う。論理学者のアルフレッド・ホーンによって導入された。ヒルベルトの時代から命題論理と第一階述語論理の任意の普遍妥当な論理式は、公理と推論規則をうまく定めれば機械的にすべて導出することができることは判明していたがその効率は非常に悪かった。エルブランの定理の改良として1965年にロビンソンが導出原理（resolution principle）にもとづく導出法（resolution）を提案した。Kowalski はKowalski(1974)の中で論理式をプログラムと見る立場を明確に述べ、その際に改めて論理プログラミングの世界に導入された中心的概念がホーン節（Horn clause）である。ホーン節は論理プログラミングの基本であり、プログラミング言語の Prolog, GHC のコードは表記として第二形式のホーン節そのものである。ホーン節は計算複雑性理論にも関連する。ホーン節の論理積が真となるような各変数の値の組合せを探す問題はP完全問題であり、ホーン充足可能性問題（HORNSAT）とも呼ばれる。これはNP完全問題の1つである充足可能性問題のサブセットである。命題論理における原子命題を P とするとき、P または ¬P のことをリテラル（literal）と呼び、リテラルを選言（disjunction）で結合したものを節（せつ、clause）と呼ぶ。例えば、L , L , ... , L をリテラルとするとその選言結合は節である。命題論理における節（clause）がであるとき、この節をホーン節（Horn clause）と呼ぶ。論理プログラミングにおいては、「否定を含まないリテラルが一つの節」を確定節（definite clause）、「否定を含むリテラルのみからなる節」をゴール節（goal clause）と呼ぶ。すなわち、論理プログラミングにおいては、確定節とゴール節のことをホーン節と呼ぶ。ところで、命題論理においては P , Q を原子命題とすれば、は恒真命題である。すなわち、¬P ∨ Q は P → Q で置き換えることができる。確定節とゴール節は → 結合子を用いて以下のように表わされる。なお、確定節の右辺の命題 C は前提 { A , ... , A } から導かれる論理的帰結（logical consequence）と呼ぶ。

出典:wikipedia