ホーン節

ホーン節（ホーンせつ、英: 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]。

脚注

^ Horn(1951)
^ 第一階述語論理においては、述語の引数としてなにか個体を取ったもの（命題）を考える。
^ 山崎(2000) p.64
^ 第五世代コンピュータプロジェクトにおいて開発された並列論理型言語GHC（Guarded Horn Clauses；ガード付きホーン節）のHorn Clauses とはこのホーン節である。
^ 等価性の確認
P₁ ∧ P₂ ∧ ... ∧ P_n → Q

= ¬(P₁ ∧ P₂ ∧ ... ∧ P_n) ∨ Q

= ¬P₁ ∨ ¬P₂ ∨ ... ∨ ¬P_n ∨ Q
^ ヒルベルトとその学生アッケルマンがその共著「記号論理学の基礎（Grundzüge der theoretischen Logik）」において定義したように、命題論理において、公理である前提の複合命題 A₁ , A₂ , ... , A_m から複合命題 C が導出可能であるとは、
(A₁ ∧ A₂ ∧ ... ∧ A_m) → C
が恒真命題（tautology）であることを言う。つまりは、ホーン節（確定節）が恒真であれば、当然のことながら論理的帰結 C は前提から導出可能であるとなる。
^ 第一形式を単純に左右入れ替えたものである。prolog などは記法の関係上、第二形式が用いられる。数理論理学的には特に差はなく同一視してよい。
^ 等価性の確認
P₁ ∧ P₂ ∧ ... ∧ P_n →

= ¬(P₁ ∧ P₂ ∧ ... ∧ P_n) （形式的な置き換え）

= ¬P₁ ∨ ¬P₂ ∨ ... ∨ ¬P_n
^ （空欄）部分はなにも記号を書かないという意味である。
^ 論理的帰結として否定形のリテラルもせいぜい1つしかない節を双対ホーン節（dual-Horn clause）と呼ぶ。

参考文献

山崎進『計算論理に基づく推論ソフトウェア論』コロナ社、2000年。
長尾真、淵一博『論理と意味』 7巻、岩波書店〈岩波講座情報科学〉、1983年。
D.ヒルベルト、W.アッケルマン著、伊藤誠（訳）編『記号論理学の基礎』大阪教育図書社、1954年。
Robert Kowalski (1974), Predicate Logic as Programming Language
M. H. van Emden ,R. A. Kowalski (1976), The Semantics of Predicate Logic as a Programming Language
Alfred Horn (1951), On sentences which are true of direct unions of algebras, Journal of Symbolic Logic , 16 , 14-21

外部リンク

Alex Sakharov, Horn Clause at MathWorld

[1] Horn(1951)

[2] 第一階述語論理においては、述語の引数としてなにか個体を取ったもの（命題）を考える。

[3] 山崎(2000) p.64

[4] 第五世代コンピュータプロジェクトにおいて開発された並列論理型言語GHC（Guarded Horn Clauses；ガード付きホーン節）のHorn Clauses とはこのホーン節である。

[5] 等価性の確認
P₁ ∧ P₂ ∧ ... ∧ P_n → Q

= ¬(P₁ ∧ P₂ ∧ ... ∧ P_n) ∨ Q

= ¬P₁ ∨ ¬P₂ ∨ ... ∨ ¬P_n ∨ Q

[6] ヒルベルトとその学生アッケルマンがその共著「記号論理学の基礎（Grundzüge der theoretischen Logik）」において定義したように、命題論理において、公理である前提の複合命題 A₁ , A₂ , ... , A_m から複合命題 C が導出可能であるとは、
(A₁ ∧ A₂ ∧ ... ∧ A_m) → C
が恒真命題（tautology）であることを言う。つまりは、ホーン節（確定節）が恒真であれば、当然のことながら論理的帰結 C は前提から導出可能であるとなる。

[7] 第一形式を単純に左右入れ替えたものである。prolog などは記法の関係上、第二形式が用いられる。数理論理学的には特に差はなく同一視してよい。

[8] 等価性の確認
P₁ ∧ P₂ ∧ ... ∧ P_n →

= ¬(P₁ ∧ P₂ ∧ ... ∧ P_n) （形式的な置き換え）

= ¬P₁ ∨ ¬P₂ ∨ ... ∨ ¬P_n

[9] （空欄）部分はなにも記号を書かないという意味である。

[10] 論理的帰結として否定形のリテラルもせいぜい1つしかない節を双対ホーン節（dual-Horn clause）と呼ぶ。

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]