解決（ロジック）

数理論理学と自動定理証明において、導出とは命題論理と一階述語論理の文に対する反証完全な定理証明手法につながる推論規則である。命題論理の場合、導出規則を体系的に適用することは、論理式の不満足性の決定手順として機能し、ブール充足可能性問題（の補問題）を解決する。一階述語論理の場合、導出は一階述語論理の不満足性問題に対する半アルゴリズムの基礎として使用でき、ゲーデルの完全性定理に従うものよりも実用的な方法を提供する。

解決規則はデイビスとパトナム（1960）に遡ることができる。 ^[1]しかし、彼らのアルゴリズムでは、与えられた式のすべての基本インスタンスを試す必要があった。この組み合わせ爆発の原因は、1965年にジョン・アラン・ロビンソンの統語的統一アルゴリズムによって排除され、これにより、反論の完全性を保つために必要な範囲で、証明中に「オンデマンド」で式をインスタンス化することが可能になった。^[2]

解決規則によって生成される節は、解決子と呼ばれることもあります。

命題論理における解決規則は、補数リテラルを含む2 つの節によって暗示される新しい節を生成する単一の有効な推論規則です。リテラルは命題変数または命題変数の否定です。2 つのリテラルは、一方が他方の否定である場合に補数であると言われます (以下では、 は の補数とみなされます)。結果として得られる節には、補数を持たないすべてのリテラルが含まれます。正式には、 次のようになります。${\displaystyle \lnotc}$${\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に追加され、さらに解決推論を行うために考慮されます。
• 解決規則を適用した後に空の節が導出される場合は、元の式は満たされない（または矛盾する）ため、最初の推測は公理から導かれると結論付けることができます。
• 一方、空の節を導出できず、解決規則を適用してもそれ以上の新しい節を導出できない場合、その推測は元の知識ベースの定理ではありません。

このアルゴリズムの一例は、オリジナルのDavis-Putnam アルゴリズムです。このアルゴリズムは後に、解決子の明示的な表現の必要性を排除した DPLL アルゴリズムに改良されました。

この解決手法の説明では、解決導出を表す基礎データ構造としてセットS を使用しています。リスト、ツリー、有向非巡回グラフは、他の可能な一般的な代替手段です。ツリー表現は、解決ルールがバイナリであるという事実に忠実です。節の連続表記法とともに、ツリー表現により、解決ルールが、アトミックカットフォーミュラに制限されたカットルールの特殊なケースとどのように関連しているかが明確になります。ただし、ツリー表現は、空の節の導出で複数回使用される節の冗長なサブ導出を明示的に示すため、セット表現やリスト表現ほどコンパクトではありません。グラフ表現は、節の数に関してリスト表現と同じくらいコンパクトにすることができ、各リゾルベントを導出するためにどの節が解決されたかに関する構造情報も格納します。

${\displaystyle {\frac {a\vee b,\quad \neg a\vee c}{b\vee c}}}$

平易な言葉で言うと、 は偽であると仮定します。前提が真であるためには、 が真でなければなりません。あるいは、 は真であると仮定します。前提が真であるためには、が真でなければなりません。したがって、 の偽りか真偽に関わらず、両方の前提が成り立つ場合、結論は真です。 ${\displaystyle a}$${\displaystyle a\vee b}$${\displaystyle b}$${\displaystyle a}$${\displaystyle \neg a\vee c}$${\displaystyle c}$${\displaystyle a}$${\displaystyle b\vee c}$

解決規則は次のように一階述語論理に一般化できる。^[5]

${\displaystyle {\frac {\Gamma _{1}\cup \left\{L_{1}\right\}\,\,\,\,\Gamma _{2}\cup \left\{L_{2}\right\}}{(\Gamma _{1}\cup \Gamma _{2})\phi }}\phi }$

ここで、はおよびの最も一般的な単一化子であり、と には共通の変数はありません。 ${\displaystyle \phi }$${\displaystyle L_{1}}$${\displaystyle {\overline {L_{2}}}}$${\displaystyle \Gamma _{1}}$${\displaystyle \Gamma _{2}}$

節およびは、統一子としてこの規則を適用できます。 ${\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]}$解決されたリテラルの最も一般的な統合子です。

一階述語論理では、解決によって、論理的推論の従来の三段論法が1 つの規則に凝縮されます。

解決がどのように機能するかを理解するために、項論理の次の例の三段論法を考えてみましょう。

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

ホーマーはギリシャ人です。

したがって、ホーマーはヨーロッパ人です。

あるいは、より一般的には:

${\displaystyle \forall x.P(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 (ア)

2番目の節では、Xは非束縛変数であり、aは束縛値（項）である。この2つを統合すると、置換

X ↦ア

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

質問(え)

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

クレタ人は全員島民です。

島民は全員嘘つきだ。

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

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

∀ 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つのリテラルで構成されているため、各可能な解決子も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}}}$

上記の解決規則の一般化は、元の式が節標準形である必要がないように考案されている。^{[8] [9] [10] [11] [12] [13]}

これらの技術は、中間結果の式の可読性を維持することが重要である対話型の定理証明で主に有用である。さらに、節形式への変換中の組み合わせ爆発を回避し、^{[10] : 98}、解決ステップを節約することもある。^{[13] : 425}

命題論理については、マレー^{[9] :18}とマンナとウォルディンガー^{[10] :98が}次の規則を用いている。

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

ここで、 は任意の式を表し、 はを部分式として含む式を表し、はのすべての出現を に置き換えることによって構築されます。についても同様です。 解決子は、 などの規則を使用して簡略化されることが意図されています。 役に立たない自明な解決子が生成されないようにするために、が とにそれぞれ少なくとも 1 つの「負」と「正」の^[14]出現を持つ場合にのみ、規則が適用されます。 Murray は、この規則が適切な論理変換規則によって拡張されると完全であることを示しました。^{[10] : 103}${\displaystyle p}$${\displaystyle F[p]}$${\displaystyle p}$${\displaystyle F[{\textit {true}}]}$${\displaystyle F[p]}$${\displaystyle p}$${\displaystyle {\textit {true}}}$${\displaystyle G}$${\displaystyle F[{\textit {true}}]\lor G[{\textit {false}}]}$${\displaystyle q\land {\textit {true}}\implies q}$${\displaystyle p}$${\displaystyle F}$${\displaystyle G}$

トラウゴットはルールを使用する

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

ここで、 の指数はその出現の極性を示す。と は前と同じように構築されるが、の各正と各負の出現をそれぞれ と に置き換えることによって式が得られる。マレーのアプローチと同様に、適切な単純化変換が解決子に適用されるべきである。トラウゴットは、が式で使用される唯一の接続詞である限り、彼の規則が完全であることを証明した。 ^{[12] : 398–400}${\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] : 395}さらに、新しい二項接続子を導入しないため、繰り返し解決で節形式になる傾向が避けられる。ただし、小さな がより大きなおよび/またはに何度も置き換えられると、式が長くなる可能性がある。^{[12] : 398}${\displaystyle p}$${\displaystyle G[{\textit {true}}]}$${\displaystyle G[{\textit {false}}]}$

例えば、ユーザーが与えた仮定から始めると

${\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)の含意を利用して、ステップ(12)の非原子式として使用することができる。マレーの規則を使用すると、意味的に同等な式は(7)として得られたが、その統語形式のためにとして使用できなかった。${\displaystyle p}$ ${\displaystyle a\rightarrow e}$${\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 }$

トラウゴットの規則は、との複数の異なる部分式が、 という最も一般的な統一子を持つ限り、一般化される。一般化された解決子は、親式に適用することで得られるため、命題バージョンが適用可能になる。トラウゴットの完全性証明は、この完全に一般的な規則が使用されているという仮定に依存している。^{[12] : 401}彼の規則がとに制限された場合に完全であるかどうかは明らかではない。^[16]${\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 }$${\displaystyle p_{1}=\cdots =p_{m}}$${\displaystyle p_{m+1}=\cdots =p_{n}}$

パラモジュレーションは、述語記号が等号である節の集合を推論するための関連技術である。これは、反射的な同一性を除き、節のすべての「等しい」バージョンを生成する。パラモジュレーション操作は、等号リテラルを含む必要がある肯定的なfrom節を取り、次に、等号の片側と統合する部分項を持つinto節を検索する。次に、部分項は等号のもう一方の側で置き換えられる。パラモジュレーションの一般的な目的は、システムを原子に縮小し、置換時に項のサイズを縮小することです。^[17]

• カリーヌ
• ジーケーシー
• カワウソ
• 諺9
• 皮肉
• スパス
• 吸血鬼
• Logictools オンライン証明

• 凝縮分離 - 解決の初期バージョン
• 帰納的論理プログラミング
• 逆解像度
• 論理プログラミング
• 分析的タブロー法
• SLD解像度
• 解像度の推論

• Robinson , J. Alan (1965). 「解決原理に基づくマシン指向ロジック」Journal of the ACM . 12 (1): 23–41. doi : 10.1145/321250.321253 . S2CID  14389185.
• Leitsch, Alexander (1997)。The Resolution Calculus 。理論計算機科学テキスト。EATCS シリーズ。Springer。ISBN 978-3-642-60605-2。
• Gallier, Jean H. (1986). コンピュータサイエンスのための論理: 自動定理証明の基礎. Harper & Row .
• Lee, Chin-Liang Chang , Richard Char-Tung (1987)。記号論理と機械的定理証明。Academic Press。ISBN 0-12-170350-9。{{cite book}}: CS1 maint: multiple names: authors list (link)

• Alex Sakharov。「解決原理」。MathWorld。
• Alex Sakharov。「解決」。MathWorld。