CARINE
その他の用法については「 カリーヌ 」をご覧（2021年12月） “CARINE”
CARINE (Computer Aided Reasoning Engine)は、一次 古典論理 自動定理証明器です。これは当初、深さ優先検索ベースのアルゴリズムにおける戦略遅延句構築 (DCC) および属性シーケンス (ATS) の強化効果の研究のために構築されました。 CARINE の主な検索アルゴリズムは、反復的に深化する深さ優先検索 (深さ優先反復深化 (DFID) とも呼ばれます) に基づく半線形解像度 (SLR) であり、次のような定理証明で使用されます。テオ。 SLR は DCC を使用して高い推論率を達成し、ATS を使用して検索スペースを削減します。
コンテンツ
1 遅延条項の構築 (DCC)
1.1 DCC はどのように機能しますか?
2 属性シーケンス (ATS)
3 参考文献
4 外部リンク
遅延条項の構築 (DCC)
節の遅延構築は、節を構築する作業を最小限に抑えることで、定理証明者のパフォーマンスを向上させる失速戦略です。適用された推論規則のすべての結論 (節) を構築する代わりに、そのような節を構築するための情報は、定理証明者が節を破棄するか構築するかを決定するまで一時的に保存されます。定理証明者が節を保持することを決定した場合、それは構築されてメモリに保存されます。そうでない場合、節を構築するための情報は消去されます。推論された句を構築できる情報を格納するために、追加の CPU 操作はほとんど必要ありません。ただし、句の作成には多くの時間がかかる場合が一部の定理証明者は、節の作成と削除に総実行時間の 30% ～ 40% を費やしています。DCC を使用すると、この無駄な時間を節約できます。
DCC は、あまりにも多くの中間節 (特に 1 次節) が短期間に作成されて破棄される場合に役立ちます。これは、そのような短命の節を作成するために実行される操作が回避されるためです。DCC は、命題節のみの定理ではあまり効果的ではない場合が
DCC はどのように機能しますか?
推論規則を適用するたびに、特定の変数を項 (たとえばx f ( a ) ) で置換する必要があり、置換セットが形成されます。結果の節を構築して置換セットを破棄する代わりに、定理証明者は、推論規則にどの節が含まれているか、どの推論規則が適用されたかなど、他の情報とともに置換セットを単純に維持し、結果を構築せずに導出を続行します。推論規則の節。この手順は、定理の証明者が、特定の基準とヒューリスティックに基づいて、導出の最終節 (およびおそらくパスに沿った他の節) を構築するか破棄するかを決定するポイントに到達するまで、導出に沿って進みます。派生全体、つまり、保持されている置換セットと、それらに格納されている情報をメモリから削除します。
属性シーケンス (ATS)
定理証明の節(の非公式な定義)は、そのリテラルの評価に応じて、真または偽の答えになるステートメントです。句は、リテラルの論理和(つまり、OR)、論理積(つまり、AND)、セット、またはマルチセット (セットに似ていますが、同一の要素を含むことができます) として表されます。
リテラルの選言としての句の例は次のとおりです。 ¬ 裕福( よ) ∨ ¬
頭いい( よ) ∨ ¬
美しい( よ) ∨
大好き(X よ ) { lnot operatorname {裕福} (Y)lor lnot operatorname {賢い} (Y)lor lnot operatorname {美しい} (Y)lor operatorname {loves} (X，Y)}
シンボルの場所 ∨ { lor}
と ¬
{ lnot }
は、それぞれ
logical orおよび
logical notです。
上記の例では、Yが裕福でスマートで美しい場合、XはYを愛していることを示しています。ただし、 XとYが誰であるかはわかりません。上記の表現は、次の論理ステートメントに由来することに注意して
人間の領域に属するすべてのY ， Xについて:
裕福( よ) ∧
頭いい( よ) ∧
美しい( よ) ⟹
大好き(X よ ) { operatorname {裕福} (Y)land operatorname {賢い} (Y)land operatorname {美しい} (Y)implies operatorname {loves} (X，Y)}
形式論理のいくつかの変換規則を使用して、上記の例のリテラルの論理和を生成します。
XとYは変数です。 ¬ { lnot }
裕福な， ¬ { lnot }
スマート， ¬ { lnot }
美しい、愛は文字通りです。変数Xを定数 John に、変数Yを定数 Jane に置き換えると、上記の節は次のようになります。 ¬ 裕福( ジェーン) ∨ ¬
頭いい( ジェーン) ∨ ¬
美しい( ジェーン) ∨
大好き( ジョン ジェーン ) { lnot operatorname {裕福} ({text{Jane}})lor lnot operatorname {スマート} ({text{Jane}})lor lnot operatorname {beautiful} ({text{Jane}}) {ジェーン}})lor operatorname {loves} ({text{ジョン}}，{text{ジェーン}})}
句属性は、句の特性です。句属性の例を次に示します。
句内のリテラルの数 (つまり、句の長さ)
句内の用語記号の数
句内の定数の数
句内の変数の数
句内の関数の数
句内の否定リテラルの数
句内の正のリテラルの数
句内の個別の変数の数
句内のすべてのリテラルにおける任意の項の最大の深さ 例 条項ハ = ¬ P (X) ∨ Q( a b へ(X ) )
{ C=lnot P(x)lor Q(a，b，f(x))}
もっている：
2 つのリテラルが含まれているため、長さは 2
1 つの負のリテラル¬ P (X )
{ lnot P(x)}
Q ( a ， b ， f ( x ))である 1 つの正のリテラル
aとbの2 つの定数
2 つの変数 ( xが 2 回出現)
xである 1 つの異なる変数
fである 1 つの関数
最大項深度 2
x、a、b、f、xの5 つの用語記号
属性シーケンスは、長さ k の派生セットの射影を表す節属性の k nタプルのシーケンスです。k と n は厳密に正の整数です。派生のセットはドメインを形成し、属性シーケンスは派生と属性シーケンス間のマッピングのコドメインを形成します。 例 は、k = 3 およびn = 2 の属性シーケンスです。
これは、B1、B2、R1、B3、R2、および B4 が節である などの派生に対応します。ここでの属性は、句の長さと見なされます。
最初のペア (2，2) は、派生のペア (B1，B2) に対応します。これは、B1 の長さが 2 で、B2 の長さも 2 であることを示しています。
2 番目のペア (2，1) はペア (R1，B3) に対応し、R1 の長さが 2 で、B3 の長さが 1 であることを示します。
最後のペア (1，1) はペア (R2，B4) に対応し、R2 の長さが 1 で、B4 の長さが 1 であることを示します。
注:句属性のnタプルは、Stephan Schulz 博士 ( E 等式定理証明者を参照) によって命名された特徴ベクトルに似ています (ただし、同じではありません)。
参考文献
^ ハロウン、ポール （2005). Delayed Clause Construction and Attribute Sequences による定理証明者の強化(博士論文)。マギル大学。
^コーフ、リチャードE（1985）。「深さ優先の反復 – 深化: 最適許容ツリー検索」. 人工知能。27 : 97–109. ドイ：10.1016/0004-3702(85)90084-0 .
^ 新生児、モンティ（2001）。自動化された定理証明: 理論と実践. ニューヨーク：Springer-Verlag。ISBN 978-0-387-95075-4.
外部リンク
CARINEのウェブサイト
ACM出版
E ホームページ”