ローカルコンテキスト書き換えによる解決証明の削減

数理論理学の一分野である証明理論において、局所文脈書き換えによる解決証明簡約は、局所文脈書き換えを介した解決証明簡約の手法である。^[1]この証明圧縮手法は、解決証明の後処理として動作するReduceAndReconstructというアルゴリズムとして提示された。

ReduceAndReconstructは、サブ証明を同等かより強力な証明に変換する一連のローカル証明書き換え規則に基づいています。^[1]各規則は特定のコンテキストに合わせて定義されています。

文脈^[1]には2つのピボット（および）と5つの節（、、、および）が含まれる。文脈の構造は（1）に示されている。これは、がおよび（反対極性）に含まれ、 がおよび（これも反対極性）に含まれることを意味することに注意されたい。 ${\displaystyle p}$ ${\displaystyle q}$ ${\displaystyle \alpha}$ ${\displaystyle \beta}$ ${\displaystyle \gamma}$ ${\displaystyle \delta}$ ${\displaystyle \eta}$ ${\displaystyle p}$ ${\displaystyle \beta}$ ${\displaystyle \gamma}$ ${\displaystyle q}$ ${\displaystyle \delta}$ ${\displaystyle \alpha}$

${\displaystyle {\cfrac {{\cfrac {\beta \qquad \gamma }{\delta }}\,p\qquad \alpha }{\eta }}\,q}$

1

下の表はSimoneらが提案した書き換え規則を示している。 [ ^1]このアルゴリズムの考え方は、これらの規則を機会主義的に適用することで証明のサイズを削減することです。

コンテクスト	ルール
ケースA1:${\displaystyle s\notin \alpha ,t\in \gamma }$	${\displaystyle {\cfrac {{\cfrac {stC\qquad {\overline {s}}tD}{tCD}}\,\operatorname {var} (s)\qquad {\overline {t}}E}{CDE}}\,\operatorname {var} (t)\Rightarrow {\cfrac {{\cfrac {stC\qquad {\overline {t}}E}{sCE}}\,\operatorname {var} (t)\qquad {\cfrac {{\overline {t}}E\qquad {\overline {s}}tD}{{\overline {s}}DE}}\,\operatorname {var} (t)}{CDE}}\,\operatorname {var} (s)}$
ケースA2:${\displaystyle s\notin \alpha ,t\notin \gamma }$	${\displaystyle {\cfrac {{\cfrac {stC\qquad {\overline {s}}D}{tCD}}\,\operatorname {var} (s)\qquad {\overline {t}}E}{CDE}}\,\operatorname {var} (t)\Rightarrow {\cfrac {{\cfrac {stC\qquad {\overline {t}}E}{sCE}}\,\operatorname {var} (t)\qquad {\overline {s}}D}{CDE}}\,\operatorname {var} (s)}$
ケースB1:${\displaystyle s\in \alpha ,t\in \gamma }$	${\displaystyle {\cfrac {{\cfrac {stC\qquad {\overline {s}}tD}{tCD}}\,\operatorname {var} (s)\qquad s{\overline {t}}E}{sCDE}}\,\operatorname {var} (t)\Rightarrow {\cfrac {stC\qquad s{\overline {t}}E}{sCE}}\,\operatorname {var} (t)}$
ケースB2:${\displaystyle s\in \alpha ,t\notin \gamma }$	${\displaystyle {\cfrac {{\cfrac {stC\qquad {\overline {s}}D}{tDC}}\,\operatorname {var} (s)\qquad s{\overline {t}}E}{sCDE}}\,\operatorname {var} (t)\Rightarrow {\cfrac {{\cfrac {stC\qquad s{\overline {t}}E}{sCE}}\,\operatorname {var} (t)\qquad {\overline {s}}D}{CDE}}\,\operatorname {var} (s)}$
ケースB3:${\displaystyle {\overline {s}}\in \alpha ,t\notin \gamma }$	${\displaystyle {\cfrac {{\cfrac {stC\qquad {\overline {s}}D}{tDC}}\,\operatorname {var} (s)\qquad {\overline {s}}{\overline {t}}E}{{\overline {s}}CDE}}\,\operatorname {var} (t)\Rightarrow {\overline {s}}D}$
ケースA1'	${\displaystyle {\cfrac {{\cfrac {stC\qquad {\overline {s}}tD}{tCD}}\,\operatorname {var} (s)\qquad {\overline {t}}E}{CDE}}\,\operatorname {var} (t)\Leftarrow {\cfrac {{\cfrac {stC\qquad {\overline {t}}E}{sCE}}\,\operatorname {var} (t)\qquad {\cfrac {{\overline {t}}E\qquad {\overline {s}}tD}{{\overline {s}}DE}}\,\operatorname {var} (t)}{CDE}}\,\operatorname {var} (s)}$
ケースB2':${\displaystyle t\notin \gamma }$	${\displaystyle {\cfrac {{\cfrac {stC\qquad {\overline {s}}D}{tCD}}\,\operatorname {var} (s)\qquad s{\overline {t}}E}{sCDE}}\,\operatorname {var} (t)\Rightarrow {\cfrac {stC\qquad s{\overline {t}}E}{sCE}}\,\operatorname {var} (t)}$

最初の5つのルールは以前の論文で紹介されました。^[2]さらに:

• ルールA2はそれ自体では何の縮約も行いません。しかし、他のルールを適用する新たな機会を生み出す「シャッフル」効果があるため、依然として有用です。
• ルール A1 は証明のサイズが大きくなる可能性があるため、実際には使用されません。
• 規則 B1、B2、B2'、および B3 は、元のルート節よりも強力な変換されたルート節を生成するため、直接的に削減の役割を果たします。
• B規則の適用は、変換されたルート節に欠落しているリテラルが、証明ルートへの経路における別の解決ステップで関与する可能性があるため、不正な証明につながる可能性があります（下の例を参照）。したがって、このような状況が発生した場合、アルゴリズムは正当な証明を「再構築」する必要があります。

次の例^[1]は、 B2'規則を適用した後に証明が違法になる状況を示しています。

${\displaystyle {\cfrac {{\cfrac {{\cfrac {{\cfrac {\mathbf {pq} \qquad \mathbf {{\overline {p}}o} }{\mathbf {qo} }}\,p\qquad \mathbf {p{\overline {q}}} }{\mathbf {po} }}\,q\qquad {\cfrac {qr\qquad {\overline {p}}{\overline {q}}}{{\overline {p}}r}}\,q}{or}}\,p\qquad {\overline {o}}s}{rs}}\,o}$

2

強調表示されたコンテキストにルールB2'を適用します。

${\displaystyle {\cfrac {{\cfrac {{\cfrac {\mathbf {pq} \qquad \mathbf {p{\overline {q}}} }{\mathbf {p} }}\,q\qquad {\cfrac {qr\qquad {\overline {p}}{\overline {q}}}{{\overline {p}}r}}\,q}{or}}\,p\qquad {\overline {o}}s}{rs}}\,o}$

3

変換されたルート節からリテラルが欠落しているため、証明は不正です。証明を再構成するには、最後の解決ステップ（これは冗長です）と一緒に削除します。最終的な結果は、以下の合法的（かつより強力な）証明です。 ${\displaystyle o}$ ${\displaystyle o}$

${\displaystyle {\cfrac {{\cfrac {pq\qquad p{\overline {q}}}{p}}\,q\qquad {\cfrac {qr\qquad {\overline {p}}{\overline {q}}}{{\overline {p}}r}}\,q}{r}}\,p}$

4

規則A2を適用することでこの証明をさらに簡略化し、規則B2'を適用する新たな機会を作り出す。^[1]

通常、ルールA2が適用されるコンテキストは膨大に存在するため、網羅的なアプローチは一般的には実現不可能です。一つの提案^[1]は、反復回数とタイムアウト（最初に到達したもの）という2つの終了基準を持つループとして実行することですReduceAndReconstruct。以下の擬似コード^[1]はこれを示しています。

1  関数ReduceAndReconstruct( /* 証明 */ , timelimit , maxIterations ):${\displaystyle \pi }$  
 2       i = 1 からmaxIterations まで
 3 ループの削減と再構築();
 4           if  time > timelimit  then         // タイムアウト
 5               break ;
 6      エンド、 
 7  エンド機能

ReduceAndReconstruct以下に指定される関数 を使用するReduceAndReconstructLoop。アルゴリズムの最初の部分では、解決グラフの位相的な順序付けを行う（エッジが先行ノードから解決ノードへと向かうことを考慮する）。これは、各ノードがその先行ノードの後に​​訪問されることを保証するためである（これにより、破損した解決ステップが常に検出され、修正される）。^[1]

1  関数ReduceAndReconstructLoop( /* 証明 */ ):${\displaystyle \pi }$  
 2       TS = トポロジカルソート( );${\displaystyle \pi }$ TS 
 4          内の各ノードがリーフでない場合は
 3      ${\displaystyle n}$    ${\displaystyle n}$ 
 5 の              場合、 6 
 =                   Resolution( , );${\displaystyle n_{\text{piv}}\in n_{\text{clause}}^{\text{left}}}$ ${\displaystyle {\overline {n_{\text{piv}}}}\in n_{\text{clause}}^{\text{right}}}$  ${\displaystyle n_{\text{clause}}}$ ${\displaystyle n_{\text{clause}}^{\text{left}}}$ ${\displaystyle n_{\text{clause}}^{\text{right}}}$ 
 7 の左コンテキストがあればそれを決定する。${\displaystyle n}$ 
 8 の適切なコンテキスト（存在する場合）を決定します。${\displaystyle n}$ 
 9 ヒューリスティックに 1 つのコンテキスト (存在する場合) を選択し、対応するルールを適用します。
10               else if  and then 
11 ;に置き換えます${\displaystyle n_{\text{piv}}\notin n_{\text{clause}}^{\text{left}}}$ ${\displaystyle {\overline {n_{\text{piv}}}}\in n_{\text{clause}}^{\text{right}}}$  ${\displaystyle n}$ ${\displaystyle n^{\text{left}}}$ 
12               else if  and then 
13 ;に置き換えます${\displaystyle n_{\text{piv}}\in n_{\text{clause}}^{\text{left}}}$ ${\displaystyle {\overline {n_{\text{piv}}}}\notin n_{\text{clause}}^{\text{right}}}$  ${\displaystyle n}$ ${\displaystyle n^{\text{right}}}$ 
14               else if  and then 
15 経験的に先行詞またはを選択;${\displaystyle n_{\text{piv}}\notin n_{\text{clause}}^{\text{left}}}$ ${\displaystyle {\overline {n_{\text{piv}}}}\notin n_{\text{clause}}^{\text{right}}}$  ${\displaystyle n^{\text{left}}}$ ${\displaystyle n^{\text{right}}}$ 
16またはに置き換えます。${\displaystyle n}$ ${\displaystyle n^{\text{left}}}$ ${\displaystyle n^{\text{right}}}$ 
17      終了
18  終了関数

入力証明が木でない場合（一般に、解決グラフは有向非巡回グラフである）、コンテキストの節は複数の解決ステップに関与する可能性があります。この場合、書き換え規則の適用が他の解決ステップに影響を与えないようにするための安全な解決策は、節で表されるノードのコピーを作成することです。^[1]この解決策は証明のサイズを増加させるため、実行時には注意が必要です。 ${\displaystyle \delta }$ ${\displaystyle \delta }$

ルール選択のヒューリスティックは、良好な圧縮性能を実現するために重要です。Simoneら ^[1]は、与えられたコンテキストに該当する場合、ルールの優先順位として以下の順序を採用しています：B2 > B3 > { B2', B1 } > A1' > A2（X > Yは、XがYよりも優先されることを意味します）。

実験では、ReduceAndReconstructのみでは、RecyclePivotsアルゴリズムよりも圧縮率/時間比が劣ることが示されています。^[3]ただし、RecyclePivotsはプルーフに1回しか適用できませんが、ReduceAndReconstructは複数回適用することでより良い圧縮率を得ることができます。ReduceAndReconstructとRecyclePivotsアルゴリズムを組み合わせる試みは、良好な結果をもたらしました。^[1]

注記

1. Simone, SF; Brutomesso, R.; Sharygina, N.「解決証明削減への効率的かつ柔軟なアプローチ」第6回ハイファ検証会議、2010年。
2. Bruttomesso, R.; Rollini, S.; Sharygina, N.; Tsitovich, A.「局所証明変換による柔軟な補間」国際コンピュータ支援設計会議、2010年。
3. Bar-Ilan, O.; Fuhrmann, O.; Hoory, S.; Shacham, O.; Strichman, O.「解決証明の線形時間縮約」HVC、2008年。