シータ包含

シータ包含（θ包含、または単に包含）は、2つの1階述語論理節間の決定可能な関係であり、一方の節が他方の節を論理的に含意することを保証する。これは1965年にジョン・アラン・ロビンソンによって初めて導入され、帰納論理プログラミングにおける基本的な概念となっている。ある節が別の節をθ包含するかどうかを判定することは、NP完全問題である。

節、すなわち一階述語論理リテラルの選言は、そのすべての選言要素を含む集合と考えることができる。

この慣習では、条項${\textstyle c_{1}}$θは節を包含する${\textstyle c_{2}}$代役がいる場合${\displaystyle \theta }$適用によって得られる条項${\textstyle \theta }$に${\textstyle c_{1}}$は、${\textstyle c_{2}}$[ ^{1 ]​}

θ-包含関係は論理的含意よりも弱い関係であり、つまり、節が${\textstyle c_{1}}$θは節を包含する ${\textstyle c_{2}}$、 それから${\textstyle c_{1}}$論理的に必然的に${\textstyle c_{2}}$しかし、その逆は真ではない。ある節は別の節を論理的に含意することはできるが、θ-包含することはできない。

θ-包含は決定可能である。より正確には、ある節が別の節をθ-包含するかどうかの問題は、節の長さに関してNP完全である。これは、設定をホーン節のペアに限定した場合でも依然として真である。^{[ 2 ]}

ホーン節間の二項関係として、θ包含関係は反射的かつ推移的です。したがって、前順序を定義します。異なる節が互いに構文的変種になり得るため、反対称ではありません。しかし、互いにθ包含関係にある節の同値類には、変数名の変更を除いて一意の最短節が存在し、これは効率的に計算できます。この同値関係に関する商のクラスは完全束であり、無限上昇鎖と無限下降鎖の両方を持ちます。この束の部分集合は、精緻化グラフ。 ^{[ 3 ]}

θ-包含関係は、 1965 年にJ. Alan Robinsonによって分解の文脈で初めて導入され、^{[ 4 ]} 1970 年にGordon Plotkinによって節の集合の最小一般化を見つけて削減するために帰納的論理プログラミングに初めて適用されました。 ^{[ 5 ]} 1977 年に Lewis D. Baxter は θ-包含関係が NP 完全であることを証明し、^{[ 6 ]} 1979 年の NP 完全問題に関する画期的な研究であるComputers and Intractabilityでは、これを NP 完全問題のリストに含めています。^{[ 2 ]}

分解計算または重ね合わせ計算に基づく定理証明器は、冗長な節を剪定するために θ-包含関係を使用します。^{[ 7 ]}さらに、θ-包含関係は帰納的論理プログラミングで使用される最も重要な含意の概念であり、ある節が別の節の特殊化か一般化かを判断するための基本的なツールです。^{[ 1 ]} また、ある節が例をカバーしているかどうかをテストしたり、与えられた節のペアが冗長であるかどうかを判断したりするためにも使用されます。^{[ 2 ]}

• バクスター、ルイス・デンバー（1977年9月）。統一の複雑性（PDF）（学位論文）。ウォータールー大学。
• De Raedt, Luc (2008).論理的および関係的学習. 認知技術. ベルリン、ハイデルベルク: Springer. Bibcode : 2008lrl..book.....D . doi : 10.1007/978-3-540-68856-3 . ISBN 978-3-540-20040-6。
• Kietz, Jörg-Uwe; Lübbe, Marcus (1994). 「帰納論理プログラミングのための効率的な包含アルゴリズム」 . Machine Learning Proceedings 1994. Elsevier. pp. 130–138 . doi : 10.1016/b978-1-55860-335-6.50024-6 . ISBN  97815586033562023年11月26日に取得。
• Plotkin, Gordon D. (1970).自動帰納推論法(PDF) (博士論文). エジンバラ大学. hdl : 1842/6656 .
• Robinson, JA (1965). "分解原理に基づく機械指向論理" . Journal of the ACM . 12 (1): 23– 41. doi : 10.1145/321250.321253 . S2CID 14389185 . 
• Waldmann, Uwe; Tourret, Sophie; Robillard, Simon; Blanchette, Jasmin (2022年11月) 「飽和定理証明のための包括的なフレームワーク」 Journal of Automated Reasoning . 66 (4): 499–539 . doi : 10.1007/s10817-022-09621-7 . ISSN 0168-7433 . PMC 9637109. PMID 36353684 .