導出原理
述語論理のリテラルには個体変数が含まれるため、リテラルと否定リテラルとを単純に比較するだけでは削除できるかどうか分からない。一階述語論理ではリテラルと否定リテラルそれぞれの原子論理式が単一化できる場合に導出を行う。
また、導出の対象となる節は、冠頭標準形にして存在記号を削除したスコーレム連言標準形の論理式である。
例えば、一方の節がリテラル p ( x , y ) {\displaystyle p(x,y)} 、もう一方の節がリテラル ¬ p ( z , f ( b ) ) {\displaystyle \lnot p(z,f(b))} を含む場合、適切な代入 σ = { z / x , y / f ( b ) } {\displaystyle \sigma =\left\{z/x,y/f(b)\right\}} により各リテラルは p ( x , f ( b ) ) {\displaystyle p(x,f(b))} 、 ¬ p ( x , f ( b ) ) {\displaystyle \lnot p(x,f(b))} と書き換えられ、同じにすることができる。ここで代入 { z / x , y / f ( b ) } {\displaystyle \left\{z/x,y/f(b)\right\}} は z → x {\displaystyle z\to x} 、 y → f ( b ) {\displaystyle y\to f(b)} に書き換えることを表す。
導出は2つの節を前提として導出節を導くものであるので、どの節に導出規則を適用するかについては様々な選択肢があり、そのやり方により効率が大幅に異なる。代表的な証明戦略として以下のものがある。
線形導出(linear resolution)
前提となる節の一方を、頂上節(top clause)として指定した節と、頂上節から導出された節に限定する方法。導出木を書くと導出の流れが線状に一列に並ぶため、線形導出と呼ばれる。論理プログラミング言語の代表であるPrologで用いられるSLD導出(Selective Linear resolution for Definite clause)は線形導出の一種である。
入力導出(input resolution)
前提となる節の一方を最初に与えられた節集合の要素(導出された節以外の節)に限定する方法。
支持集合戦略(set-of-support strategy)
あらかじめ支持集合という節の集合を指定しておき、前提となる節の一方を支持集合の節とそこから導出された節に限定する方法。節集合S、T がありS-T が充足可能であるときT はS の支持集合と言う。目標に関係ないところを探索しないよう導出の対象を制限することで、より効率的な導出を行うための手法で、1965年に Lawrence Wos らが提案した。
意味導出(semantic resolution)
論理式のモデルあるいは解釈を利用して導出の対象を制限し、探索の空間を狭めることで効率的な導出を行う手法。特定のモデルにおいて真となる可能性がある節と偽となる可能性のある節とを親節に選ぶ Slagle の Semantic Clash resolution など様々な方法がある。
同様に、 p → q {\displaystyle p\to q} 、 q → r {\displaystyle q\to r} の節形式 ¬ p ∨ q {\displaystyle \lnot p\lor q} 、 ¬ q ∨ r {\displaystyle \lnot q\lor r} による三段論法は以下のようになる。
C 1 = ¬ p ∨ q ( p → q ) C 2 = ¬ q ∨ r ( q → r ) C R = ¬ p ∨ r ( r e s o l v e n t , p → r ) {\displaystyle {\begin{array}{ll}C_{1}=\lnot p\lor q&\left(p\to q\right)\\C_{2}=\lnot q\lor r&\left(q\to r\right)\\C_{R}=\lnot p\lor r&\left(\mathrm {resolvent,\ } p\to r\right)\end{array}}}