ホーン節
読み方：ほーんせつ
【英】：Horn clause
【英】：Horn clause
リテラル(命題そのものか, またはその否定)が選言で結合された論理式を節と呼び, 正のリテラル(否定のついていない命題)を高々1つ含む節のことをホーン節と呼ぶ. Prolog などの多くの論理型プログラムはホーン節の集合として構成される. 任意の論理式は等価な節集合に変換できるが, 特にホーン節のみからなる節集合に対しての定理証明手続きは, 線形導出などの効率的な手続きが存在することが知られている.
「OR事典」の他の用語
| 近似・知能・感覚的手法： | プロダクション規則 ベイジアンラフ集合 ホップフィールドネットワーク ホーン節 メタヒューリスティクス ラフセット ラフメンバシップ値 |
ホーン節
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/09/01 16:02 UTC 版)
ホーン節（ホーンせつ、英: Horn clause）とは、数理論理学において、節（リテラルの選言結合命題）のうち、肯定形のリテラルの数が1つ以下の物を言う。論理学者のアルフレッド・ホーンによって導入された[1]。
- ^ Horn(1951)
- ^ 第一階述語論理においては、述語の引数としてなにか個体を取ったもの（命題）を考える。
- ^ 山崎(2000) p.64
- ^ 第五世代コンピュータプロジェクトにおいて開発された並列論理型言語GHC（Guarded Horn Clauses；ガード付きホーン節）のHorn Clauses とはこのホーン節である。
- ^ 等価性の確認
- P1 ∧ P2 ∧ ... ∧ Pn → Q
- = ¬(P1 ∧ P2 ∧ ... ∧ Pn) ∨ Q
- = ¬P1 ∨ ¬P2 ∨ ... ∨ ¬Pn ∨ Q
- ^ ヒルベルトとその学生アッケルマンがその共著「記号論理学の基礎（Grundzüge der theoretischen Logik）」において定義したように、命題論理において、公理である前提の複合命題 A1 , A2 , ... , Am から複合命題 C が導出可能であるとは、
- (A1 ∧ A2 ∧ ... ∧ Am) → C
- ^ 第一形式を単純に左右入れ替えたものである。prolog などは記法の関係上、第二形式が用いられる。数理論理学的には特に差はなく同一視してよい。
- ^ 等価性の確認
- P1 ∧ P2 ∧ ... ∧ Pn →
- = ¬(P1 ∧ P2 ∧ ... ∧ Pn) （形式的な置き換え）
- = ¬P1 ∨ ¬P2 ∨ ... ∨ ¬Pn
- ^ （空欄）部分はなにも記号を書かないという意味である。
- ^ 論理的帰結として否定形のリテラルもせいぜい1つしかない節を双対ホーン節（dual-Horn clause）と呼ぶ。
[続きの解説]
ホーン節（Horn clause）
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/06/20 22:13 UTC 版)
「ホーン節」の記事における「ホーン節（Horn clause）」の解説
命題論理における節（clause）が 否定を含まないリテラルが一つの節（例：L1 ∨ ¬L2 ∨ ... ∨ ¬Ln） または、 否定を含むリテラルのみからなる節（例：¬L1 ∨ ¬L2 ∨ ... ∨ ¬Ln） であるとき、この節をホーン節（Horn clause）と呼ぶ。
※この「ホーン節（Horn clause）」の解説は、「ホーン節」の解説の一部です。
「ホーン節（Horn clause）」を含む「ホーン節」の記事については、「ホーン節」の概要を参照ください。
ウィキペディア小見出し辞書の「ホーン節」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。 お問い合わせ。
「ホーン節」の例文・使い方・用例・文例
- ホーン節のページへのリンク
