ホーン条項

数理論理学と論理プログラミングにおいて、ホーン節は、論理プログラミング、形式仕様、普遍代数、モデル理論で使用するための有用な特性を与える特定の規則のような形式の論理式です。ホーン節は、1951年に初めてその重要性を指摘した論理学者アルフレッド・ホーンにちなんで名付けられました。 ^[1]

ホーン節は、最大 1 つの正の、つまり否定されていないリテラルを持つ選言節(リテラルの選言) です。

逆に、最大 1 つの否定リテラルを含むリテラルの論理和は、デュアルホーン節と呼ばれます。

ちょうど1つの正のリテラルを持つホーン節は、確定節または厳密なホーン節です。^[2]負のリテラルを持たない確定節は単位節です。 [ ^3]変数を持たない単位節は事実です。 [ ^4] 正のリテラルを持たないホーン節は目標節です。リテラルを含まない空の節（偽に相当）は目標節です。これらの3種類のホーン節は、次の命題例で示されています。

節内のすべての変数は暗黙的に普遍量化され、その範囲は節全体になります。したがって、たとえば次のようになります。

¬人間( X ) ∨死すべき者( X )

意味:

∀X( ¬人間( X ) ∨死すべき者( X ) )、

これは論理的には次の式と同等です。

∀X（人間（X）→死すべき者（X））。

ホーン節は、構成的論理と計算論理において基本的な役割を果たします。これらは、1 階解決による自動定理証明において重要です。2つのホーン節の解決元はホーン節であり、目標節と確定節の解決元はゴール節であるためです。ホーン節のこれらの特性により、定理の証明の効率が向上します。ゴール節はこの定理の否定です。上の表のゴール節を参照してください。直感的には、 φ を証明したい場合は、¬φ (目標) を仮定し、その仮定が矛盾を生じるかどうかを確認します。矛盾が生じる場合は、 φ が成り立つ必要があります。このように、機械的な証明ツールは、2 セット (仮定と (サブ) 目標) ではなく、1 セットの式 (仮定) のみを維持する必要があります。

命題ホーン節は計算複雑性においても興味深い問題である。命題ホーン節の連言を真にするための真理値割り当てを求める問題はHORNSATとして知られている。この問題はP完全であり線形時間で解ける。^[6]対照的に、制限のないブール充足可能性問題はNP完全問題である。

普遍代数では、明確なホーン節は一般に準恒等式と呼ばれる。準恒等式の集合によって定義可能な代数のクラスは準多様体と呼ばれ、より制限的な多様体の概念、すなわち等式クラスが持つ優れた特性のいくつかを備えている。[ ^7]モデル理論の観点からは、ホーン文は、（論理的同値性を除き）簡約積の下で保存される文とまったく同じであるため重要である。特に、直積の下で保存される。一方、ホーンではないが、任意の直積の下で保存される文もある。^[8]

ホーン節は論理プログラミングの基礎でもあり、明確な節を含意の形で記述するのが一般的です。

( p ∧ q ∧ ... ∧ t ) → u

実際、明確な節を持つ目標節を解決して新しい目標節を生成することは、論理プログラミング言語Prologの実装で使用されるSLD 解決推論規則の基礎です。

論理プログラミングでは、明確な節は目標削減手順として動作します。たとえば、上記の Horn 節は次の手順として動作します。

u を表示し、p を表示し、q を表示し、... t を表示します。

この節の逆用を強調するために、逆の形式で書かれることがよくあります。

u ← ( p ∧ q ∧ ... ∧ t )

Prologでは次のように記述されます。

u  :-  p 、 q 、 ...、 t 。

論理プログラミングでは、論理形式が

∀ X (偽← p ∧ q ∧ ... ∧ t )

解決すべき問題の否定を表します。問題自体は、肯定的なリテラルの存在量化された結合です。

∃ X ( p ∧ q ∧ ... ∧ t )

Prolog 表記法には明示的な量指定子がなく、次の形式で記述されます。

:-  p 、 q 、 ...、 t 。

この表記法は、問題の記述としても、問題の否定の記述としても読めるという意味で曖昧です。しかし、どちらの読み方も正しいです。どちらの場合も、問題を解くことは空の節を導出することと同じです。Prolog 表記法では、これは次の式を導出することと同じです。

：- 真実。

最上位の目標節を問題の否定として読むと、空節はfalseを表し、空節の証明は問題の否定の反証になります。最上位の目標節を問題そのものとして読むと、空節はtrue を表し、空節の証明は問題に解があることの証明になります。

この問題の解決方法は、解決証明から抽出できる最上位の目標節の変数Xを項で置き換えることです。このように使用すると、目標節はリレーショナル データベースの結合クエリに似ており、ホーン節ロジックは計算能力において汎用チューリング マシンと同等になります。

ヴァン・エムデンとコワルスキー（1976）は、論理プログラミングの文脈でホーン節のモデル理論的特性を調査し、すべての確定節の集合Dには一意の最小モデルMがあることを示した。原子式 AがDによって論理的に導かれるのは、AがMで真である場合に限る。したがって、存在量化された肯定リテラルの連言で表される問題P がDによって論理的に導かれるのは、 PがMで真である場合に限る。ホーン節の最小モデル意味論は、論理プログラムの安定モデル意味論の基礎である。^[9]

• 制約付きホーン節
• 命題計算

• Burris, Stanley; Sankappanavar, HP, 編 (1981)。『普遍代数の講座』。Springer -Verlag。ISBN 0-387-90578-2。
• バス、サミュエル R. (1998)。「証明理論入門」。サミュエル R. バス (編) 著。証明理論ハンドブック。論理学と数学の基礎研究。第 137 巻。エルゼビア BV pp. 1–78。doi : 10.1016/S0049-237X(98)80016-5。ISBN 978-0-444-89840-1. ISSN  0049-237X.
• チャン、チェン・チュン;キースラー、H. ジェローム(1990) [1973].モデル理論. 論理学と数学の基礎研究 (第3版). エルゼビア. ISBN 978-0-444-88054-3。
• Dowling, William F.; Gallier, Jean H. (1984). 「ホーン命題式の充足可能性をテストするための線形時間アルゴリズム」。Journal of Logic Programming . 1 (3): 267–284. doi : 10.1016/0743-1066(84)90014-1 .
• van Emden, MH ; Kowalski, RA (1976). 「プログラミング言語としての述語論理の意味論」(PDF) . Journal of the ACM . 23 (4): 733–742. CiteSeerX  10.1.1.64.9246 . doi :10.1145/321978.321991. S2CID  11048276.
• ホーン、アルフレッド(1951)。 「代数の直接和集合に当てはまる文について」。 記号論理学ジャーナル。16 (1): 14–21。doi :10.2307/2268661。JSTOR 2268661。S2CID  42534337。
• Lau, Kung-Kiu; Ornaghi, Mario (2004)。「計算ロジックにおける正しいプログラム開発のための構成単位の指定」。計算ロジックにおけるプログラム開発。コンピュータサイエンスの講義ノート。第 3049 巻。pp . 1–29。doi:10.1007 / 978-3-540-25951-0_1。ISBN 978-3-540-22152-4。
• Makowsky, JA (1987). 「コンピュータサイエンスにおいてホーン式が重要な理由: 初期構造と一般的な例」(PDF) . Journal of Computer and System Sciences . 34 (2–3): 266–292. doi : 10.1016/0022-0000(87)90027-4 .