ホーン節

ホーン節（ホーンせつ、英: Horn clause）とは、数理論理学において、節（リテラルの選言結合命題）のうち、肯定形のリテラルの数が1つ以下の物を言う。論理学者のアルフレッド・ホーンによって導入された^[1]。

概要

ヒルベルトの時代から命題論理と第一階述語論理の任意の普遍妥当な論理式は、公理と推論規則をうまく定めれば機械的にすべて導出することができることは判明していたがその効率は非常に悪かった。エルブランの定理の改良として1965年にロビンソンが導出原理（resolution principle）にもとづく導出法（resolution）を提案した。Kowalski は「Predicate Logic as Programming Language」の中で論理式をプログラムと見る立場を明確に述べ、その際に改めて論理プログラミングの世界に導入された中心的概念がホーン節（Horn clause）である。

ホーン節は論理プログラミングの基本であり、プログラミング言語の Prolog, GHC のコードは表記として第二形式のホーン節そのものである。

ホーン節は計算複雑性理論にも関連する。ホーン節の論理積が真となるような各変数の値の組合せを探す問題はP完全問題であり、ホーン充足可能性問題（HORNSAT）とも呼ばれる。これはNP完全問題の1つである充足可能性問題のサブセットである。

定義

節（clause）

命題論理における原子命題を P とするとき^[2]、P または ¬P のことをリテラル（literal）と呼び、両者を区別する場合は P を正リテラル (positive literal)、¬P を負リテラル (negative literal) と呼ぶ。リテラルを選言（disjunction）で結合したものを節（せつ、clause）と呼ぶ。例えば、L₁ , L₂ , ... , L_n をリテラルとするとその選言結合

L₁ ∨ L₂ ∨ ... ∨ L_n

は節である。

ホーン節（Horn clause）

命題論理における節が

正リテラルを一つだけ持つ （例：P₁ ∨ ¬P₂ ∨ ... ∨ ¬P_n）

または、

正リテラルを持たない （例：¬P₁ ∨ ¬P₂ ∨ ... ∨ ¬P_n）

とき、この節をホーン節（Horn clause）と呼ぶ^[3][4]。

論理プログラミングにおける用法

論理プログラミングにおいては、「正リテラルを一つだけ持つ節」を確定節（definite clause）、「正リテラルを持たない節」をゴール節（goal clause）と呼ぶ。すなわち、論理プログラミングにおいては、確定節とゴール節のことをホーン節と呼ぶ。

ところで、命題論理においては P, Q, R を原子命題とすれば、

¬P ∨ ¬Q ∨ R ≡ (P ∧ Q) → R

は恒真命題である。すなわち、¬P ∨ ¬Q ∨ R は (P ∧ Q) → R で置き換えることができる。論理プログラミングにおいては、確定節とゴール節は → 結合子を用いて以下のように表わされることが多い:

確定節（definite clause）^[5][6]

P₁ ∧ P₂ ∧ ... ∧ P_n → Q （第一形式）

Q ← P₁ ∧ P₂ ∧ ... ∧ P_n（第二形式）^[7]

ゴール節（goal clause）^[8]

P₁ ∧ P₂ ∧ ... ∧ P_n → （空欄）（第一形式）^[9]

（空欄）← P₁ ∧ P₂ ∧ ... ∧ P_n （第二形式）

同様に、原子命題 P に対して、

• (空欄) → P (これは P と同値であり、確定節である)
• P → (空欄) (これらは ¬P と同値であり、ゴール節である)

などもホーン節として正しい。なお、確定節の右辺の原始命題 Q は前提 { P₁ , ... , P_n } から導かれる論理的帰結（logical consequence）と呼ぶ^[10]。