解決（論理）

命題論理における解決規則は、相補的なリテラルを含む2 つの節から導かれる新しい節を生成する単一の有効な推論規則です。リテラルとは、命題変数または命題変数の否定です。2 つのリテラルは、一方が他方の否定である場合に相補的であると言われます (以下、 ${\displaystyle \lnot c}$は、${\displaystyle c}$結果として得られる節には、補語を持たないすべてのリテラルが含まれます。正式には次のようになります。

${\displaystyle {\frac {a_{1}\lor a_{2}\lor \cdots \lor c,\quad b_{1}\lor b_{2}\lor \cdots \lor \neg c}{a_{1}\lor a_{2}\lor \cdots \lor b_{1}\lor b_{2}\lor \cdots }}}$

どこ

全て${\displaystyle a_{i}}$、${\displaystyle b_{i}}$、 そして${\displaystyle c}$リテラルです。

区切り線は「～を伴う」という意味を表しています。

上記は次のように表記することもできます。

${\displaystyle {\frac {(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow c,\quad c\rightarrow (b_{1}\lor b_{2}\lor \cdots )}{(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow (b_{1}\lor b_{2}\lor \cdots )}}}$

または模式的に表すと次のようになります。

${\displaystyle {\frac {\Gamma _{1}\cup \left\{\ell \right\}\,\,\,\,\Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}{\Gamma _{1}\cup \Gamma _{2}}}|\ell |}$

弊社では以下の用語を使用しています。

• 条項$\displaystyle \Gamma _{1}\cup \left\{\ell \right\}}$ そして$\displaystyle \Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}$推論の前提は
• ${\displaystyle \Gamma _{1}\cup \Gamma _{2}}$（前提の解決文）は、その結論である。
• 文字通り${\displaystyle \ell }$左側の解決済みリテラルは、
• 文字通り${\displaystyle {\overline {\ell }}}$正しい解決済みリテラルです。
• ${\displaystyle |\ell |}$は解決された原子またはピボットです。

解決規則によって生成される節は、 2 つの入力節の解決節と呼ばれます。これは、用語ではなく節に適用される合意の原則です。 ^{[ 3 ]}

2 つの節に複数の相補的なリテラルのペアが含まれている場合、解決ルールはそのような各ペアに対して (独立して) 適用できますが、結果は常に同義反復になります。

モーダス・ポネンスは、（1文字の節と2文字の節の）解決の特殊なケースと見なすことができる。

${\displaystyle {\frac {p\rightarrow q,\quad p}{q}}}$

と同等

${\displaystyle {\frac {\lnot p\lor q,\quad p}{q}}}$

完全な探索アルゴリズムと組み合わせることで、解決規則は命題論理式の充足可能性、ひいては一連の公理の下での文の妥当性を判定するための健全かつ完全なアルゴリズムをもたらす。

この解決手法は背理法を用い、命題論理の任意の文は連言標準形の同等の文に変換できるという事実に基づいている。^{[ 4 ]}手順は以下のとおりである。

• 知識ベース内のすべての文と、証明すべき文（推測）の否定は、連言的に結び付けられている。
• 結果として得られる文は、接続詞を節の集合Sの要素とみなした接続詞標準形に変換される。^{[ 4 ]}
  • 例えば、 ${\displaystyle (A_{1}\lor A_{2})\land (B_{1}\lor B_{2}\lor B_{3})\land (C_{1})}$セットを生み出す${\displaystyle S=\{A_{1}\lor A_{2},B_{1}\lor B_{2}\lor B_{3},C_{1}\}}$。
• 解決ルールは、相補的なリテラルを含むすべての可能な節のペアに適用されます。解決ルールを適用するたびに、結果として得られる文は、重複するリテラルを削除することによって簡略化されます。節に相補的なリテラルが含まれている場合は、その節は（同義反復として）破棄されます。含まれていない場合、かつ節セットSにまだ含まれていない場合は、 Sに追加され、さらなる解決推論の対象となります。
• 分解規則を適用した後に空節が導出される場合、元の式は充足不能（または矛盾）であり、したがって最初の予想は公理から導かれると結論付けることができる。
• 一方、空節を導出できず、かつ解決規則を適用して新たな節を導出できない場合、その推測は元の知識ベースの定理ではない。

このアルゴリズムの一例として、オリジナルのデイビス・パトナムアルゴリズムがあり、これは後にDPLLアルゴリズムへと改良され、レゾルベントの明示的な表現の必要性を排除した。

この解決手法の説明では、解決導出を表す基底データ構造として集合Sを使用します。リスト、ツリー、有向非巡回グラフも、考えられる一般的な代替手段です。ツリー表現は、解決規則が二項であるという事実に忠実です。節のシーケント表記と組み合わせることで、ツリー表現は、解決規則がアトミックカット式に限定されたカット規則の特殊なケースとどのように関連しているかを明確に示します。ただし、ツリー表現は、空節の導出で複数回使用される節の冗長な部分導出を明示的に示すため、集合表現やリスト表現ほどコンパクトではありません。グラフ表現は、節の数に関してリスト表現と同じくらいコンパクトであり、各解決項を導出するために解決された節に関する構造情報も格納します。

条項${\displaystyle P(x),Q(x)}$そして${\displaystyle \neg P(b)}$このルールを適用できます${\displaystyle [b/x]}$統一者として。

ここで、xは変数、bは定数です。

${\displaystyle {\frac {P(x),Q(x)\,\,\,\,\neg P(b)}{Q(b)}}[b/x]}$

ここで私たちは

• 条項${\displaystyle P(x),Q(x)}$ そして${\displaystyle \neg P(b)}$推論の前提は
• ${\displaystyle Q(b)}$（前提の解決文）は、その結論である。
• 文字通り${\displaystyle P(x)}$左側の解決済みリテラルは、
• 文字通り${\displaystyle \neg P(b)}$正しい解決済みリテラルです。
• ${\displaystyle P}$は解決された原子またはピボットです。
• ${\displaystyle [b/x]}$は、解決されたリテラルの最も一般的な統一子です。

一階述語論理では、分解法は論理的推論の伝統的な三段論法を単一の規則に凝縮する。

解決の仕組みを理解するために、次の項論理の三段論法の例を考えてみましょう。

ギリシャ人は皆ヨーロッパ人である。

ホメロスはギリシャ人である。

したがって、ホメロスはヨーロッパ人である。

あるいは、より一般的に言えば：

${\displaystyle \forall xP(x)\Rightarrow Q(x)}$

${\displaystyle P(a)}$

したがって、${\displaystyle Q(a)}$

分解法を用いて推論を再構成するには、まず節を連言標準形（CNF）に変換する必要があります。この形式では、すべての量化が暗黙的になります。変数（ X、Y 、…）に対する全称量化子は省略され、存在量化変数はスコレム関数に置き換えられます。

${\displaystyle \neg P(x)\vee Q(x)}$

${\displaystyle P(a)}$

したがって、${\displaystyle Q(a)}$

そこで問題となるのは、解決手法は最初の2つの節から最後の節をどのように導き出すのか、ということだ。ルールは単純だ。

• 同じ述語を含む2つの節を見つけてください。ただし、一方の節ではその述語が否定されているが、もう一方の節では否定されていないものとします。
• 2つの述語に対して単一化を実行します。（単一化が失敗した場合は、述語の選択が間違っています。前の手順に戻ってやり直してください。）
• 統合述語で束縛されていた未束縛変数が、2つの節の他の述語にも出現する場合は、それらの変数を束縛値（項）に置き換えてください。
• 統合された述語を破棄し、2 つの節から残りの述語を組み合わせて新しい節を作成し、それらも「∨」演算子で結合します。

この規則を上記の例に適用すると、述語Pが否定形で現れることがわかります。

¬ P ( X )

最初の節では、否定形ではない

P（a）

第２節において、Xは非束縛変数であり、aは束縛値（項）である。この２つを統一すると、置換式が得られる。

X ↦ a

統一述語を破棄し、残りの述語（この場合はQ ( Xのみ）にこの置換を適用すると、次の結論が得られます。

Q（a）

別の例として、三段論法の形式を考えてみましょう。

クレタ島民は皆、島民である。

島民は全員嘘つきだ。

したがって、クレタ人は全員嘘つきである。

あるいはもっと一般的に言えば、

∀ X P ( X ) → Q ( X )

∀ X Q ( X ) → R ( X )

したがって、∀ X P ( X ) → R ( X )

CNFでは、前件は次のようになります。

¬ P ( X ) ∨ Q ( X )

¬ Q ( Y ) ∨ R ( Y )

（2番目の節の変数名は、異なる節の変数がそれぞれ異なることを明確にするために変更されました。）

さて、最初の節のQ ( X ) と2 番目の節の ¬ Q ( Y ) を統一すると、 XとY は結局同じ変数になります。これを残りの節に代入して組み合わせると、次の結論が得られます。

¬ P ( X ) ∨ R ( X )

ロビンソンによって定義された解決規則には、上記で定義された解決の適用前または適用中に、同じ節内の 2 つのリテラルを統合する因数分解も組み込まれています。結果として得られる推論規則は反駁完全であり、^{[ 6 ]}節の集合が充足不能となるのは、因数分解によって強化された解決のみを使用して空の節の導出が存在する場合のみです。

空節を導出するために因数分解が必要となる、充足不能な節集合の例は次のとおりです。

${\displaystyle {\begin{array}{rlcl}(1):&P(u)&\lor &P(f(u))\\(2):&\lnot P(v)&\lor &P(f(w))\\(3):&\lnot P(x)&\lor &\lnot P(f(x))\\\end{array}}}$

各節は 2 つのリテラルで構成されているため、可能な各解決文も同様です。したがって、因数分解なしの解決では、空の節は決して得られません。因数分解を使用すると、たとえば次のように得られます。^{[ 7 ]}

${\displaystyle {\begin{array}{rll}(4):&P(u)\lor P(f(w))&{\text{by resolving (1) and (2), with }}v=f(u)\\(5):&P(f(w))&{\text{by factoring (4), with }}u=f(w)\\(6):&\lnot P(f(f(w')))&{\text{by resolving (5) and (3), with }}w=w',x=f(w')\\(7):&{\text{false}}&{\text{by resolving (5) and (6), with }}w=f(w')\\\end{array}}}$

命題論理については、Murray ^{[ 9 ] : 18}および Manna と Waldinger ^{[ 10 ] : 98 は}次の規則を使用する。

${\displaystyle {\begin{array}{c}F[p]\;\;\;\;\;\;\;\;\;\;G[p]\\\hline F[{\textit {true}}]\lor G[{\textit {false}}]\\\end{array}}}$、

どこ${\displaystyle p}$は任意の式を表します。${\displaystyle F[p]}$そして${\displaystyle G[p]}$を含む式を表す${\displaystyle p}$サブ式として。${\displaystyle F[{\textit {true}}]}$は、すべての出現箇所を置き換えることによって構築されます。${\displaystyle p}$で${\displaystyle F[p]}$による${\displaystyle {\textit {true}}}$同様に、${\displaystyle G[{\textit {false}}]}$は、すべての出現箇所を置き換えることによって構築されます。${\displaystyle p}$で${\displaystyle G[p]}$による${\displaystyle {\textit {false}}}$. 解決剤${\displaystyle F[{\textit {true}}]\lor G[{\textit {false}}]}$次のようなルールを使用して簡略化することを意図しています${\displaystyle q\land {\textit {true}}\implies q}$など。無用な自明な解決文の生成を防ぐため、このルールは、次の場合にのみ適用されます。${\displaystyle p}$少なくとも 1 つの「否定的」および「肯定的」^{[ 14 ]}の発生がある${\displaystyle F}$そして${\displaystyle G}$それぞれ。マレーは、適切な論理変換規則を追加すればこの規則は完全であることを示した。^{[ 10 ]： 103}

トラウゴットは、同様に表現できるルールを使用している。

${\displaystyle {\begin{array}{c}F[p^{+},p^{-}]\;\;\;\;\;\;\;\;G[p]\\\hline F[G[{\textit {true}}],\lnot G[{\textit {false}}]]\\\end{array}}}$、

ここで指数は${\displaystyle p}$その発生の極性を示します。${\displaystyle G[{\textit {true}}]}$そして${\displaystyle G[{\textit {false}}]}$以前と同じように構築され、その式は${\displaystyle F[G[{\textit {true}}],\lnot G[{\textit {false}}]]}$は、各正の出現を置き換えることによって得られます。${\displaystyle p}$で${\displaystyle F}$と${\displaystyle G[{\textit {true}}]}$そして、それぞれの否定的な出来事は${\displaystyle G[{\textit {false}}]}$マレーのアプローチと同様に、レゾルベントには適切な単純化変換を適用する必要がある。トラウゴットは、以下の条件が満たされれば、彼の規則が完全であることを証明した。${\displaystyle \land ,\lor ,\rightarrow ,\lnot }$これらは数式で使用される唯一の接続詞である。^{[ 12 ]： 398-400}

トラウゴットのレゾルベントはマレーのものより強い。^{[ 12 ]： 395}さらに、新たな二項結合子を導入しないため、繰り返しのレゾルベントで節形式に陥る傾向を回避できる。ただし、小さな要素がある場合、式が長くなる可能性がある。${\displaystyle p}$より大きなものに複数回置き換えられる${\displaystyle G[{\textit {true}}]}$および/または${\displaystyle G[{\textit {false}}]}$[ ^{12 ] : 398​}

例えば、ユーザーが提示した前提から始めると

${\displaystyle {\begin{array}{rccc}(1):&a&\rightarrow &b\land c\\(2):&c&\rightarrow &d\\(3):&b\land d&\rightarrow &e\\(4):&\lnot (a&\rightarrow &e)\\\end{array}}}$

マレーのルールは、矛盾を推論するために次のように使用できます。^{[ 15 ]}

${\displaystyle {\begin{array}{rrclccl}(5):&({\textit {true}}\rightarrow d)&\lor &(a\rightarrow b\land {\textit {false}})&\implies &d\lor \lnot a&{\mbox{from (2) and (1), with }}p=c\\(6):&(b\land {\textit {true}}\rightarrow e)&\lor &({\textit {false}}\lor \lnot a)&\implies &(b\rightarrow e)\lor \lnot a&{\mbox{from (3) and (5), with }}p=d\\(7):&(({\textit {true}}\rightarrow e)\lor \lnot a)&\lor &(a\rightarrow {\textit {false}}\land c)&\implies &e\lor \lnot a\lor \lnot a&{\mbox{from (6) and (1), with }}p=b\\(8):&(e\lor \lnot {\textit {true}}\lor \lnot {\textit {true}})&\lor &\lnot ({\textit {false}}\rightarrow e)&\implies &e&{\mbox{from (7) and (4), with }}p=a\\(9):&\lnot (a\rightarrow {\textit {true}})&\lor &{\textit {false}}&\implies &{\textit {false}}&{\mbox{from (4) and (8), with }}p=e\\\end{array}}}$

同様の目的で、トラウゴットのルールは次のように使用できます 。^{[ 12 ]： 397}

${\displaystyle {\begin{array}{rcccl}(10):&a\rightarrow b\land ({\textit {true}}\rightarrow d)&\implies &a\rightarrow b\land d&{\mbox{from (1) and (2), with }}p=c\\(11):&a\rightarrow ({\textit {true}}\rightarrow e)&\implies &a\rightarrow e&{\mbox{from (10) and (3), with }}p=(b\land d)\\(12):&\lnot {\textit {true}}&\implies &{\textit {false}}&{\mbox{from (11) and (4), with }}p=(a\rightarrow e)\\\end{array}}}$

両方の控除額を比較すると、以下の問題点が明らかになる。

• トラウゴットのルールはより明確な解を与えるかもしれない。(5)と(10)を比較すると、どちらも(1)と(2)を解くことができる。${\displaystyle p=c}$。
• マレーの規則では、(5)、(6)、(7)に3つの新しい選言記号が導入されましたが、トラウゴットの規則では新しい記号は導入されませんでした。この点で、トラウゴットの中間式はマレーの式よりもユーザーのスタイルに近くなっています。
• 後者の問題により、トラウゴットのルールは仮定(4)の含意を利用して、${\displaystyle p}$非原子式${\displaystyle a\rightarrow e}$ステップ（12）において、マレーの規則を用いると、意味的に等価な式は次のようになる。${\displaystyle e\lor \lnot a\lor \lnot a}$（７）として得られたが、使用できなかった。${\displaystyle p}$その構文形式による。

一階述語論理の場合、マレーの規則は、異なるが統一可能な部分式を許容するように一般化される。${\displaystyle p_{1}}$そして${\displaystyle p_{2}}$の${\displaystyle F}$そして${\displaystyle G}$それぞれ。${\displaystyle \phi }$は、${\displaystyle p_{1}}$そして${\displaystyle p_{2}}$すると、一般化されたレゾルベントは${\displaystyle F\phi [{\textit {true}}]\lor G\phi [{\textit {false}}]}$より特別な置換の場合、規則は依然として有効である。${\displaystyle \phi }$が使用される場合、完全性を達成するためにそのようなルールの適用は必要ありません。

トラウゴットの規則は、互いに異なる複数の部分式を許容するように一般化されている。${\displaystyle p_{1},\ldots ,p_{m}}$の${\displaystyle F}$そして${\displaystyle p_{m+1},\ldots ,p_{n}}$の${\displaystyle G}$、 に限って${\displaystyle p_{1},\ldots ,p_{n}}$共通の最も一般的な統一子を持つ、${\displaystyle \phi }$一般化レゾルベントは、適用後に得られます。${\displaystyle \phi }$親式に、命題バージョンを適用可能にする。トラウゴットの完全性証明は、この完全に一般的な規則が使用されるという仮定に基づいている。^{[ 12 ]： 401}制限された場合、彼の規則が完全性を維持するかどうかは明らかではない。${\displaystyle p_{1}=\cdots =p_{m}}$そして${\displaystyle p_{m+1}=\cdots =p_{n}}$[ ^{16 ]​}