Loading article…
数理論理学および論理プログラミングにおいて、ホーン節は、論理プログラミング、形式仕様、普遍代数、モデル理論で使用するのに有用な特性を持つ、特定の規則のような形式の論理式である。ホーン節は、 1951年にその重要性を初めて指摘した論理学者アルフレッド・ホーンにちなんで名付けられた。 [ 1 ]
ホーン節とは、肯定の、つまり否定されていないリテラルを最大で1つしか含まない選言節（リテラルの選言）のことである。
逆に、否定リテラルが最大で 1 つであるリテラルの選言は、デュアルホーン節と呼ばれます。
正のリテラルがちょうど 1 つ含まれるホーン節は、確定節または厳密ホーン節です。[ 2 ]負のリテラルが含まれない確定節は単位節です。[ 3 ]変数を含まない単位節は事実です。[ 4 ] 正のリテラルを含まないホーン節は目標節です。リテラルがまったく含まれていない空節 (偽と同等) は目標節です。これら 3 種類のホーン節は、次の命題の例で示されています。
節内のすべての変数は、節全体をスコープとする全称量化子として暗黙的に指定されます。例えば、次のようになります。
は以下を表します。
これは論理的に以下と同等です。
ホーン節は、構成論理と計算論理において基本的な役割を果たします。2つのホーン節の分解式がそれ自体ホーン節であり、目標節と確定節の分解式が目標節であるため、ホーン節は一階分解による自動定理証明において重要です。ホーン節のこれらの特性は、定理証明の効率を高めることにつながります。目標節はこの定理の否定です（上記の表の目標節を参照）。直感的に、φを証明したい場合、¬φ（目標）を仮定し、そのような仮定が矛盾につながるかどうかを確認します。矛盾につながる場合は、φが成立しなければなりません。このようにして、機械的な証明ツールは、2つのセット（仮定と（サブ）目標）ではなく、1つのセット（仮定）のみを維持すれば済みます。
命題ホーン節は計算複雑性においても興味深い。命題ホーン節の論理積を真にする真理値割り当てを見つける問題はHORNSATとして知られている。この問題はP完全であり、線形時間で解ける。[ 6 ]対照的に、制約のないブール充足可能性問題はNP完全問題である。
普遍代数では、確定ホーン節は一般に準恒等式と呼ばれ、準恒等式の集合によって定義可能な代数のクラスは準多様体と呼ばれ、より制限的な多様体の概念、すなわち等式クラスの優れた性質のいくつかを享受する。[ 7 ]モデル理論の観点からは、ホーン文は、簡約積の下で保存される文と（論理的同値を除いて）正確に一致するため重要である。特に、ホーン文は直積の下で保存される。一方、ホーン文ではないが、任意の直積の下で保存される文も存在する。[ 8 ]
ホーン節は論理プログラミングの基礎でもあり、そこでは明確な節を含意の形で記述するのが一般的です。
実際、目標節を確定節で解決して新しい目標節を生成することは、論理プログラミング言語Prologの実装で使用されているSLD解決推論規則の基礎となっている。
論理プログラミングにおいて、確定節は目標還元手続きとして機能します。例えば、上記のホーン節は、次の手続きとして機能します。
この節の逆用法を強調するために、しばしば逆の形で表記される。
Prologでは、これは次のように記述されます。
u :- p 、q 、...、t 。論理プログラミングでは、目標節は論理形式を持ちます。
これは、解決すべき問題の否定を表します。問題自体は、肯定リテラルの存在量化論理積です。
Prologの表記法には明示的な量指定子はなく、次の形式で記述されます。
:- p 、q 、...、t 。この表記法は、問題の記述としても、問題の否定の記述としても解釈できるという意味で曖昧です。しかし、どちらの解釈も正しいです。どちらの場合も、問題を解決することは空節を導出することに相当します。Prologの表記法では、これは以下を導出することと同等です。
：-真実。最上位の目標節が問題の否定として解釈される場合、空節は偽を表し、空節の証明は問題の否定に対する反駁となる。最上位の目標節が問題そのものとして解釈される場合、空節は真を表し、空節の証明は問題に解が存在することの証明となる。
この問題の解決策は、最上位の目標節における変数Xを項で置き換えることであり、これは分解証明から抽出できる。このように使用される目標節は、関係データベースにおける連言クエリに似ており、ホーン節論理は計算能力において万能チューリングマシンと同等である。
ヴァン・エムデンとコワルスキー（1976）は、論理プログラミングの文脈でホーン節のモデル理論的性質を調査し、確定節の集合Dには一意の最小モデルMが存在することを示した。原子式Aは、 MにおいてA が真である場合に限り、Dによって論理的に含意される。したがって、存在量化された正のリテラルの連言で表される問題Pは、 MにおいてPが真である場合に限り、Dによって論理的に含意される。ホーン節の最小モデル意味論は、論理プログラムの安定モデル意味論の基礎となる。[ 9 ]