ホーン節
ホーン節（ホーンせつ、英: Horn clause）とは、数理論理学において、節（リテラルの選言結合命題）のうち、肯定形のリテラルの数が1つ以下の物を言う。論理学者のアルフレッド・ホーンによって導入された[1]。
Contents
概要
ヒルベルトの時代から命題論理と第一階述語論理の任意の普遍妥当な論理式は、公理と推論規則をうまく定めれば機械的にすべて導出することができることは判明していたがその効率は非常に悪かった。エルブランの定理の改良として1965年にロビンソンが導出原理（resolution principle）にもとづく導出法（resolution）を提案した。Kowalski はKowalski(1974)の中で論理式をプログラムと見る立場を明確に述べ、その際に改めて論理プログラミングの世界に導入された中心的概念がホーン節（Horn clause）である。
ホーン節は論理プログラミングの基本であり、プログラミング言語の Prolog, GHC のコードは表記として第二形式のホーン節そのものである。
ホーン節は計算複雑性理論にも関連する。ホーン節の論理積が真となるような各変数の値の組合せを探す問題はP完全問題であり、ホーン充足可能性問題（HORNSAT）とも呼ばれる。これはNP完全問題の1つである充足可能性問題のサブセットである。
定義
節（clause）
命題論理における原子命題を P とするとき[2]、P または ¬P のことをリテラル（literal）と呼び、リテラルを選言（disjunction）で結合したものを節（せつ、clause）と呼ぶ。例えば、L1 , L2 , ... , Ln をリテラルとするとその選言結合
- L1 ∨ L2 ∨ ... ∨ Ln
は節である。
ホーン節（Horn clause）
命題論理における節（clause）が
- 否定を含まないリテラルが一つの節（例：L1 ∨ ¬L2 ∨ ... ∨ ¬Ln）
- または、
- 否定を含むリテラルのみからなる節（例：¬L1 ∨ ¬L2 ∨ ... ∨ ¬Ln）
であるとき、この節をホーン節（Horn clause）と呼ぶ[3][4]。
論理プログラミングにおける用法
論理プログラミングにおいては、「否定を含まないリテラルが一つの節」を確定節（definite clause）、「否定を含むリテラルのみからなる節」をゴール節（goal clause）と呼ぶ。すなわち、論理プログラミングにおいては、確定節とゴール節のことをホーン節と呼ぶ。
ところで、命題論理においては P , Q を原子命題とすれば、
- ¬P ∨ Q = P → Q
は恒真命題である。すなわち、¬P ∨ Q は P → Q で置き換えることができる。確定節とゴール節は → 結合子を用いて以下のように表わされる。
- 確定節（definite clause）[5][6]
- L1 ∧ L2 ∧ ... ∧ Ln → C（第一形式）
- C ← L1 ∧ L2 ∧ ... ∧ Ln（第二形式）[7]
- ゴール節（goal clause）[8]
- L1 ∧ L2 ∧ ... ∧ Ln → （空欄）（第一形式）[9]
- （空欄）← L1 ∧ L2 ∧ ... ∧ Ln （第二形式）
なお、確定節の右辺の命題 C は前提 { A1 , ... , An } から導かれる論理的帰結（logical consequence）と呼ぶ[10]。
脚注
- ↑ Horn(1951)
- ↑ 第一階述語論理においては、述語の引数としてなにか個体を取ったもの（命題）を考える。
- ↑ 山崎(2000) p.64
- ↑ 第五世代コンピュータプロジェクトにおいて開発された並列論理型言語GHC（Guarded Horn Clauses；ガード付きホーン節）のHorn Clauses とはこのホーン節である。
- ↑ 等価性の確認
- L1 ∧ L2 ∧ ... ∧ Ln → C
- = ¬(L1 ∧ L2 ∧ ... ∧ Ln) ∨ C
- = ¬L1 ∨ ¬L2 ∨ ... ∨ ¬Ln ∨ C
- ↑ ヒルベルトとその学生アッケルマンがその共著「記号論理学の基礎（Grundzüge der theoretischen Logik）」において定義したように、命題論理において、公理である前提の複合命題 A1 , A2 , ... , Am から複合命題 C が導出可能であるとは、
- (A1 ∧ A2 ∧ ... ∧ Am) → C
- ↑ 第一形式を単純に左右入れ替えたものである。prolog などは記法の関係上、第二形式が用いられる。数理論理学的には特に差はなく同一視してよい。
- ↑ 等価性の確認
- L1 ∧ L2 ∧ ... ∧ Ln →
- = ¬(L1 ∧ L2 ∧ ... ∧ Ln) （形式的な置き換え）
- = ¬L1 ∨ ¬L2 ∨ ... ∨ ¬Ln
- ↑ （空欄）部分はなにも記号を書かないという意味である。
- ↑ 論理的帰結として否定形のリテラルもせいぜい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