ホーン節

ホーン節とは

ホーン節（Horn clause）とは、数理論理学において、節（リテラルの選言結合命題）の一種であり、その中でも特に、肯定形のリテラル（正リテラル）の数が1つ以下のものを指します。この概念は、論理学者のアルフレッド・ホーンによって導入されました。

概要

命題論理と第一階述語論理において、任意の普遍的に妥当な論理式は、適切な公理と推論規則を用いることで機械的に導出可能であることが知られていましたが、その効率は非常に低いという問題がありました。

1965年、ロビンソンは導出原理（resolution principle）に基づく導出法（resolution）を提案し、エルブランの定理を改良しました。さらに、コワルスキーは「Predicate Logic as Programming Language」の中で、論理式をプログラムとして捉える視点を提示し、ホーン節を論理プログラミングの中心概念として導入しました。この考え方は、論理プログラミング言語のPrologやGHCの基礎となっています。

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

定義

節（clause）

命題論理において、原子命題Pに対し、Pまたは¬Pをリテラルと呼びます。Pを正リテラル、¬Pを負リテラルと区別します。リテラルを選言（∨）で結合したものを節と呼びます。例えば、L1, L2, ..., Ln をリテラルとすると、その選言結合 L1 ∨ L2 ∨ ... ∨ Ln は節です。

ホーン節（Horn clause）

ホーン節は、節の中でも次のいずれかの条件を満たすものを指します。

1. 正リテラルを一つだけ持つ節（例：P1 ∨ ¬P2 ∨ ... ∨ ¬Pn）
2. 正リテラルを持たない節（例：¬P1 ∨ ¬P2 ∨ ... ∨ ¬Pn）

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

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

命題論理では、原子命題P, Q, Rに対し、¬P ∨ ¬Q ∨ R ≡ (P ∧ Q) → R という恒真命題が成り立ちます。したがって、¬P ∨ ¬Q ∨ Rは(P ∧ Q) → Rで置き換えることができます。論理プログラミングでは、確定節とゴール節は、→ 結合子を用いて以下のように表現されることが一般的です。

確定節（definite clause）

第一形式：P1 ∧ P2 ∧ ... ∧ Pn → Q
第二形式：Q ← P1 ∧ P2 ∧ ... ∧ Pn

これは「P1かつP2かつ…かつPnならばQ」と解釈されます。第二形式は、Prologなどのプログラミング言語でよく用いられる表記です。

ゴール節（goal clause）

第一形式：P1 ∧ P2 ∧ ... ∧ Pn → (空欄)
第二形式：(空欄) ← P1 ∧ P2 ∧ ... ∧ Pn

これは「P1かつP2かつ…かつPnを証明せよ」という目標を表します。第二形式は、Prologなどのプログラミング言語でのクエリに対応します。

さらに、原子命題Pに対して、

(空欄) → P (Pと同値で、確定節)
P → (空欄) (¬Pと同値で、ゴール節)

もホーン節として扱われます。

確定節の右辺の原始命題Qは、前提{P1, ..., Pn}から導かれる論理的帰結と呼ばれます。

まとめ

ホーン節は、数理論理学の基礎概念であり、特に論理プログラミングにおいて重要な役割を果たします。確定節とゴール節という二つの形式を持ち、論理的推論をプログラムとして記述するための基盤となっています。Prologなどの言語は、このホーン節の構造をベースに設計されており、その重要性は多岐にわたります。

参考文献

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

関連項目

数理論理学
命題論理
述語論理
導出原理
* 論理プログラミング

もう一度検索