ホーン節

ホーン節（英: Horn clause）とは、数理論理学において、せいぜい1つの肯定形のリテラルを持つ節（リテラルの論理和）である。論理学者アルフレッド・ホーンは1951年、"On sentences which are true of direct unions of algebras" という論文（Journal of Symbolic Logic, 16, 14-21）の中で、このような節の重要性を初めて指摘した。

1つの肯定形のリテラルを持つホーン節を確定節（definite clause）と呼ぶ。肯定形のリテラルを持たないホーン節を目的節（goal clause）と呼ぶこともある。これらの呼称は主に論理プログラミングで使われる。ホーン式（Horn formula）とは、各節が全てホーン節となっている乗法標準形の論理式であり、言い換えればホーン節の論理積である。否定形のリテラルもせいぜい1つしかない節を二重ホーン節（dual-Horn clause）と呼ぶ。ホーン節は論理プログラミングの基本であり、構築主義論理にとっても重要である。

次の例は（確定）ホーン節である。

$\neg p \or \neg q \vee \cdots \vee \neg t \vee u$

このような論理式は次のように含意形式で表現しても等価である。

$(p \wedge q \wedge \cdots \wedge t) \rightarrow u$

導出による定理証明において、2つのホーン節から導出されるものもホーン節になるという関係がある。さらに、目的節と確定節から導出されるものは目的節となる。自動定理証明において、これらの事実が定理証明の効率化に寄与している（定理は目的節の形式で表される）。

実際、確定節を使って目的節から新たな目的節を導出するのが論理プログラミングの基本であり、プログラミング言語Prologの基本である。論理プログラミングでは、確定節は目的導出手続きとして作用する。例えば、上で例示したホーン節は次のような手続きになる。

$u$ であることを示すためには、$p$ を示し、かつ $q$ を示し、$\cdots$ かつ $t$ を示す。

このような節の逆向きの利用を強調するため、以下のような記法で書かれることが多い。

$u \leftarrow (p \and q \and \cdots \and t)$

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

参考文献

• Alfred Horn, （1951年） "On sentences which are true of direct unions of algebras", Journal of Symbolic Logic, 16, 14-21.

この記述は GNU Free Documentation License のもとに公開されているコンピュータ用語辞典『 Free On-line Dictionary of Computing (FOLDOC) 』に基づいています。

外部リンク

• Alex Sakharov, Horn Clause at MathWorld