圧縮耐性

節の分解証明を見てみましょう${\displaystyle \left\{a,b,c\right\}}$節の集合から

${\displaystyle \left\{\eta _{1}:\left\{a,b,p\right\},\eta _{2}:\left\{c,\neg p\right\}\right\}\quad {\frac {\eta _{1}:a,b,p\quad \quad \eta _{2}:c,\neg p}{\eta _{3}:a,b,c}}p}$

ここでは次のことが分かります。

• $\displaystyle \eta _{1}}$そして$\displaystyle \eta _{2}}$これらは入力ノードです。
• ノード$\displaystyle \eta _{3}}$支点がある${\displaystyle p}$、
  • 左に解決されたリテラル${\displaystyle p}$
  • 正しい解決済みリテラル${\displaystyle \neg p}$
• $\displaystyle \eta _{3}}$結論は節です${\displaystyle \left\{a,b,c\right\}}$
• $\displaystyle \eta _{3}}$前提はノードの結論である$\displaystyle \eta _{1}}$そして$\displaystyle \eta _{2}}$（その両親）
• DAGは

${\displaystyle {\begin{array}{ccc}\eta _{1}&&\eta _{2}\\&\nwarrow \nearrow \\&\eta _{3}\end{array}}}$

• $\displaystyle \eta _{1}}$そして$\displaystyle \eta _{2}}$の親である$\displaystyle \eta _{3}}$
• $\displaystyle \eta _{3}}$の子供です$\displaystyle \eta _{1}}$そして$\displaystyle \eta _{2}}$
• $\displaystyle \eta _{3}}$証明の根

Cの（分解）反駁は、${\displaystyle \bot }$Cから。ノードが与えられた場合、それは一般的です。${\displaystyle \eta }$条項を参照する${\displaystyle \eta }$または${\displaystyle \eta }$の節は、の結論の節を意味します。${\displaystyle \eta }$、そして（サブ）証明${\displaystyle \eta }$（サブ）証明が${\displaystyle \eta }$その唯一の根として。

いくつかの研究では、分解推論の代数的表現が見られる。分解は$\displaystyle \kappa _{1}}$そして$\displaystyle \kappa _{2}}$ピボット付き${\displaystyle p}$次のように表すことができます${\displaystyle \kappa _{1}\odot _{p}\kappa _{2}}$ピボットが一意に定義されている場合、または無関係な場合は、それを省略して単に記述します。${\displaystyle \kappa _{1}\odot \kappa _{2}}$このように、節の集合は可換演算子を持つ代数と見なすことができ、対応する項代数の項は、通常のグラフ表記よりも簡潔で、分解証明を記述するのに便利な表記法で分解証明を表します。

最後の例では、DAGの表記は次のようになります。${\displaystyle \left\{a,b,p\right\}\odot _{p}\left\{c,\neg p\right\}}$または単に${\displaystyle \left\{a,b,p\right\}\odot \left\{c,\neg p\right\}.}$

特定することができます$\displaystyle \underbrace {\overbrace {\left\{a,b,p\right\}} ^{\eta _{1}}\odot \overbrace {\left\{c,\neg p\right\}} ^{\eta _{2}}} _{\eta _{3}}}$。