解決（論理）

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

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

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

命題論理における解決

解決ルール

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

{\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 }}

どこ

、、およびはすべてリテラルです。

a_{i}

b_{i}

c

境界線は「含む」を表します。

上記は次のようにも表記されます。

{\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 )}}

あるいは図式的に言えば次のようになります:

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

次のような用語があります。

節と節は推論の前提である $\Gamma _{1}\cup \left\{\ell \right\}$ $\Gamma _{2}\cup \left\{{\overline {\ell }}\right\}$
$\Gamma _{1}\cup \Gamma _{2}$ （前提の解決者は）その結論です。
リテラルは左解決されたリテラルであり、 $\ell$
リテラルは右解決されたリテラルであり、 ${\overline {\ell }}$
$|\ell |$ 解決されたアトムまたはピボットです。

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

2 つの節に複数の補完リテラルのペアが含まれている場合、解決規則は各ペアに対して (独立して) 適用できますが、結果は常にトートロジーになります。

モーダス・ポネンスは、（1 つのリテラル節と 2 つのリテラル節の）解決の特殊なケースとして考えることができます。

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

は以下と同等である

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

解決テクニック

完全な検索アルゴリズムと組み合わせると、解決規則は命題式の充足可能性を判定する健全で完全なアルゴリズムを生成し、さらには公理セットの下での文の妥当性も判定します。

この解決手法は背理法による証明を使用し、命題論理の任意の文が連言標準形の同等の文に変換できるという事実に基づいています。^[4]手順は次のとおりです。

知識ベース内のすべての文と証明する文の否定（推測）は接続詞的に接続されています。
結果として得られる文は、接続詞を節の集合Sの要素として見た接続詞標準形に変換される。 ^[4]
- たとえば、は集合を生み出します。 $(A_{1}\lor A_{2})\land (B_{1}\lor B_{2}\lor B_{3})\land (C_{1})$ $S=\{A_{1}\lor A_{2},B_{1}\lor B_{2}\lor B_{3},C_{1}\}$
解決規則は、相補リテラルを含むすべての可能な節のペアに適用されます。解決規則の各適用後、結果として得られる文は、重複するリテラルを削除することで簡略化されます。節に相補リテラルが含まれている場合、その節は（トートロジーとして）破棄されます。相補リテラルが含まれていない場合、かつ節集合Sにまだ含まれていない場合、その節はSに追加され、さらなる解決推論のために考慮されます。
解決規則を適用した後に空の節が導出される場合は、元の式は満たされない（または矛盾する）ため、最初の推測は公理から導かれると結論付けることができます。
一方、空の節を導出できず、解決規則を適用してもそれ以上の新しい節を導出できない場合、その推測は元の知識ベースの定理ではありません。

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

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

簡単な例

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

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

一階論理における解決

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

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

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

例

節およびは、統一子としてこの規則を適用できます。 $P(x),Q(x)$ $\neg P(b)$ $[b/x]$

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

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

ここでわかるのは

節と節は推論の前提である $P(x),Q(x)$ $\neg P(b)$
$Q(b)$ （前提の解決者は）その結論です。
リテラルは左解決されたリテラルであり、 $P(x)$
リテラルは右解決されたリテラルであり、 $\neg P(b)$
$P$ 解決されたアトムまたはピボットです。
$[b/x]$ 解決されたリテラルの最も一般的な統合子です。

非公式な説明

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

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

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

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

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

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

\forall x.P(x)\Rightarrow Q(x)

P(a)

したがって、

Q(a)

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

\neg P(x)\vee Q(x)

P(a)

したがって、

Q(a)

では、解決法はどのようにして最初の2つの節から最後の節を導き出すのでしょうか？そのルールは簡単です。

同じ述語を含む 2 つの節を検索します。一方の節では述語が否定されていますが、もう一方の節では否定されていません。
2つの述語の統合を実行します。(統合が失敗した場合は、述語の選択が間違っています。前の手順に戻って再試行してください。)
統一された述語で束縛されていた束縛されていない変数が 2 つの節の他の述語にも出現する場合は、そこでも束縛された値 (項) に置き換えます。
統合された述語を破棄し、2 つの節の残りの述語を「∨」演算子で結合した新しい節に結合します。

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

¬ P ( X )

最初の節では、非否定形で

P ( a )

2番目の節では、Xは束縛されていない変数であり、aは束縛された値（項）である。これら2つを統合すると、置換は次のようになる。

X ↦ a

統一された述語を破棄し、この置換を残りの述語（この場合は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]、因数分解によって強化された解決のみを用いた空節の導出が存在する場合にのみ、節の集合は充足不可能となる。

空の節を導き出すために因数分解が必要となる不満足な節集合の例は次のようになります。

{\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]

{\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が以下の規則を用いている。

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

、

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

トラウゴットはこのルールを使う

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

、

ここで、の指数はその出現の極性を示す。とは前述と同様に構築されるが、におけるの正の出現と負の出現をそれぞれとに置き換えることで、式が得られる。マレーのアプローチと同様に、の解決子には適切な単純化変換を適用する。トラウゴットは、が式で使用される接続詞のみである限り、彼の規則が完全であることを証明した。^[12]^{: 398–400} $p$ $G[{\textit {true}}]$ $G[{\textit {false}}]$ $F[G[{\textit {true}}],\lnot G[{\textit {false}}]]$ $p$ $F$ $G[{\textit {true}}]$ $G[{\textit {false}}]$ $\land ,\lor ,\rightarrow ,\lnot$

トラウゴットの解決法はマレーの解決法よりも強力である。^[12]^{: 395}さらに、新たな二項接続子を導入しないため、繰り返し解決において節形式になる傾向を回避できる。しかし、小さながより大きなand/orに何度も置き換えられると、式が長くなる可能性がある。^[12]^{: 398} $p$ $G[{\textit {true}}]$ $G[{\textit {false}}]$

命題的非節解決の例

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

{\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]

{\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}

{\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)をで解決していることがわかる。 $p=c$
マレーの規則は、(5)、(6)、(7)の3つの新しい選言記号を導入しましたが、トラウゴットの規則は新しい記号を導入しませんでした。この意味で、トラウゴットの中間式は、マレーのものよりもユーザーのスタイルに近いと言えます。
後者の問題に対し、トラウゴットの規則は仮定(4)の含意を利用し、ステップ(12)の非原子式として使用することができます。マレーの規則を用いると、意味的に等価な式( 7 )が得られますが、その統語形式のために使用することはできません。 $p$ $a\rightarrow e$ $e\lor \lnot a\lor \lnot a$ $p$

第一階述語論理における非節解決

一階述語論理において、マレーの規則は一般化され、それぞれとの、異なるが統一可能な部分式とを許容する。がとの最も一般的な統一子である場合、一般化された解決子はである。より特殊な置換が用いられても規則は健全であるが、完全性を達成するためにそのような規則の適用は必要ない。^[^要出典^] $p_{1}$ $p_{2}$ $F$ $G$ $\phi$ $p_{1}$ $p_{2}$ $F\phi [{\textit {true}}]\lor G\phi [{\textit {false}}]$ $\phi$

トラウゴットの規則は、との複数の異なる部分式が、共通の最も一般的な統一子、例えばを持つ限り、複数存在できるように一般化される。一般化された解決子は、親式に適用することで得られるため、命題版が適用可能となる。トラウゴットの完全性証明は、この完全に一般的な規則が用いられるという仮定に基づいている。^[12]^{: 401}この規則がとに限定された場合にも完全性を保つかどうかは明らかではない。^[16] $p_{1},\ldots ,p_{m}$ $F$ $p_{m+1},\ldots ,p_{n}$ $G$ $p_{1},\ldots ,p_{n}$ $\phi$ $\phi$ $p_{1}=\cdots =p_{m}$ $p_{m+1}=\cdots =p_{n}$

パラモジュレーション

パラモジュレーションは、述語記号が等号である節集合の推論における関連技術である。これは、反射的な恒等式を除く、すべての「等しい」バージョンの節を生成する。パラモジュレーション演算は、等号リテラルを含む正のfrom節を取り、次に、等号の片側と単一化する部分項を持つinto節を検索する。そして、その部分項は等号のもう片側で置き換えられる。パラモジュレーションの一般的な目的は、システムを原子にまで縮小し、置換時に項のサイズを縮小することである。^[17]

実装

カリーヌ
GKC
カワウソ
箴言9
スナーク
スパス
吸血鬼
Logictoolsオンライン証明器

参照

注記

^ デイビス, マーティン; パトナム, ヒラリー (1960). 「数量化理論のための計算手順」. J. ACM . 7 (3): 201– 215. doi : 10.1145/321033.321034 . S2CID 31888376.ここでは、p. 210、「III. 原子式の消去規則」です。
^ ロビンソン 1965
^ DE Knuth,コンピュータプログラミングの芸術 4A :組み合わせアルゴリズム、パート1、p. 539
^ ab Leitsch 1997、p. 11「推論方法自体を適用する前に、式を量指定子のない連言標準形に変換します。」
^ アリス、エンリケ P.;ゴンザレス、フアン L.ルビオ、フェルナンド M. (2005)。ロジカコンピュタシオナル。エディシオネス・パラインフォ、SA ISBN 9788497321822。
^ ラッセル、スチュアート・J.、ノーヴィグ、ピーター (2009). 『人工知能：現代的アプローチ』（第3版）. プレンティス・ホール. p. 350. ISBN 978-0-13-604259-4。
^ ダフィー、デイビッド・A. (1991). 『自動定理証明の原理』ワイリー. ISBN 978-0-471-92784-6。77ページを参照。この例は、自明ではない因数分解置換を示すために若干修正されている。明瞭にするために、因数分解のステップ(5)は別個に示されている。ステップ(6)では、 (5)と(6)の単一化を可能にするためにfresh 変数が導入されており、これは(7)に必要なものである。 $w'$
^ Wilkins, D. (1973). QUEST: 非節定理証明システム（修士論文）. エセックス大学.
^ ab Murray, Neil V. (1979年2月). 量指定子を含まない非節一階述語論理の証明手順（技術報告）. シラキュース大学電気工学・コンピュータサイエンス学科. 39.（マンナ、ウォルディンガー、1980年より引用：「非節一階述語論理の証明手順」1978年）
^ abcd Manna, Zohar ; Waldinger, Richard (1980年1月). 「演繹的アプローチによるプログラム合成」. ACM Transactions on Programming Languages and Systems . 2 : 90–121 . doi :10.1145/357084.357090. S2CID 14770735.
^ Murray, NV (1982). 「完全に非節定理な定理証明」.人工知能. 18 : 67–85 . doi :10.1016/0004-3702(82)90011-x.
^ abcdef Traugott, J. (1986). 「Nested Resolution」.第8回国際自動演繹会議. CADE 1986. LNCS .第230巻. Springer. pp. 394– 403. doi :10.1007/3-540-16780-3_106. ISBN 978-3-540-39861-5。
^ ab Schmerl, UR (1988). 「数式ツリーに関する決議」. Acta Informatica . 25 (4): 425– 438. doi :10.1007/bf02737109. S2CID 32702782.まとめ
^ これらの概念は「極性」と呼ばれ、の上に現れる明示的または暗黙的な否定の数を指します。例えば、とではが正に、とではが負に、では両極性でが存在します。 $p$ $p$ $(p\land q)\lor r$ $q\rightarrow p$ $\lnot (p\land q)\lor r$ $p\rightarrow q$ $p\leftrightarrow q$
^ " " は解決後の簡略化を示すために使用されます。 $\implies$
^ ここで、「」は、名前の変更を法とする構文用語の等価性を表す。 $=$
^ Nieuwenhuis, Robert; Rubio, Alberto (2001). 「7. パラモジュレーションに基づく定理証明」(PDF) . Robinson, Alan JA; Voronkov, Andrei (編). Handbook of Automated Reasoning. Elsevier. pp. 371– 444. ISBN 978-0-08-053279-0。

参考文献

ロビンソン、J. アラン (1965). 「解決原理に基づく機械指向論理」. Journal of the ACM . 12 (1): 23– 41. doi : 10.1145/321250.321253 . S2CID 14389185.
ライチュ、アレクサンダー (1997). 『レゾリューション計算』. 理論計算機科学テキスト. EATCSシリーズ.シュプリンガー. ISBN 978-3-642-60605-2。
ガリエ、ジャン・H. (1986). 『コンピュータサイエンスのための論理：自動定理証明の基礎』ハーパー＆ロウ社.
リー、チン・リャン・チャン、リチャード・チャー・タン（1987年）『記号論理と機械的定理証明』アカデミック・プレス、ISBN 0-12-170350-9。{{cite book}}: CS1 maint: multiple names: authors list (link)

外部リンク

アレックス・サハロフ. 「解決原理」. MathWorld .
アレックス・サハロフ. 「解像度」. MathWorld .

[1] デイビス, マーティン; パトナム, ヒラリー (1960). 「数量化理論のための計算手順」. J. ACM . 7 (3): 201– 215. doi : 10.1145/321033.321034 . S2CID 31888376.ここでは、p. 210、「III. 原子式の消去規則」です。

[2] ロビンソン 1965

[3] DE Knuth,コンピュータプログラミングの芸術 4A :組み合わせアルゴリズム、パート1、p. 539

[leitsch-4] Leitsch 1997、p. 11「推論方法自体を適用する前に、式を量指定子のない連言標準形に変換します。」

[5] アリス、エンリケ P.;ゴンザレス、フアン L.ルビオ、フェルナンド M. (2005)。ロジカコンピュタシオナル。エディシオネス・パラインフォ、SA ISBN 9788497321822。

[6] ラッセル、スチュアート・J.、ノーヴィグ、ピーター (2009). 『人工知能：現代的アプローチ』（第3版）. プレンティス・ホール. p. 350. ISBN 978-0-13-604259-4。

[7] ダフィー、デイビッド・A. (1991). 『自動定理証明の原理』ワイリー. ISBN 978-0-471-92784-6。77ページを参照。この例は、自明ではない因数分解置換を示すために若干修正されている。明瞭にするために、因数分解のステップ(5)は別個に示されている。ステップ(6)では、 (5)と(6)の単一化を可能にするためにfresh 変数が導入されており、これは(7)に必要なものである。 $w'$

[8] Wilkins, D. (1973). QUEST: 非節定理証明システム（修士論文）. エセックス大学.

[Murray.1979-9] Murray, Neil V. (1979年2月). 量指定子を含まない非節一階述語論理の証明手順（技術報告）. シラキュース大学電気工学・コンピュータサイエンス学科. 39.（マンナ、ウォルディンガー、1980年より引用：「非節一階述語論理の証明手順」1978年）

[Manna.Waldinger.1980-10] Manna, Zohar ; Waldinger, Richard (1980年1月). 「演繹的アプローチによるプログラム合成」. ACM Transactions on Programming Languages and Systems . 2 : 90–121 . doi :10.1145/357084.357090. S2CID 14770735.

[11] Murray, NV (1982). 「完全に非節定理な定理証明」.人工知能. 18 : 67–85 . doi :10.1016/0004-3702(82)90011-x.

[Traugott.1986-12] Traugott, J. (1986). 「Nested Resolution」.第8回国際自動演繹会議. CADE 1986. LNCS .第230巻. Springer. pp. 394– 403. doi :10.1007/3-540-16780-3_106. ISBN 978-3-540-39861-5。

[Schmerl.1988-13] Schmerl, UR (1988). 「数式ツリーに関する決議」. Acta Informatica . 25 (4): 425– 438. doi :10.1007/bf02737109. S2CID 32702782.まとめ

[14] これらの概念は「極性」と呼ばれ、の上に現れる明示的または暗黙的な否定の数を指します。例えば、とではが正に、とではが負に、では両極性でが存在します。 $p$ $p$ $(p\land q)\lor r$ $q\rightarrow p$ $\lnot (p\land q)\lor r$ $p\rightarrow q$ $p\leftrightarrow q$

[15] " " は解決後の簡略化を示すために使用されます。 $\implies$

[16] ここで、「」は、名前の変更を法とする構文用語の等価性を表す。 $=$

[Rubio-17] Nieuwenhuis, Robert; Rubio, Alberto (2001). 「7. パラモジュレーションに基づく定理証明」(PDF) . Robinson, Alan JA; Voronkov, Andrei (編). Handbook of Automated Reasoning. Elsevier. pp. 371– 444. ISBN 978-0-08-053279-0。