一階述語論理での導出
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/10/21 06:25 UTC 版)
述語論理のリテラルには個体変数が含まれるため、リテラルと否定リテラルとを単純に比較するだけでは削除できるかどうか分からない。一階述語論理ではリテラルと否定リテラルそれぞれの原子論理式が単一化できる場合に導出を行う。 また、導出の対象となる節は、冠頭標準形にして存在記号を削除したスコーレム連言標準形の論理式である。 例えば、一方の節がリテラル 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)} に書き換えることを表す。 一般に論理式 F 1 , F 2 {\displaystyle F_{1},F_{2}} を等しくする代入を F 1 , F 2 {\displaystyle F_{1},F_{2}} の単一化子（unifier）といい、そのうち最も一般的な単一化子（最汎単一化子）を F 1 , F 2 {\displaystyle F_{1},F_{2}} のmgu（most general unifier）という。上記の例の場合、両方の論理式を等しくする代入は { z / a , y / f ( b ) , x / a } {\displaystyle \left\{z/a,y/f(b),x/a\right\}} 、 { z / x , y / c , f ( b ) / c } {\displaystyle \left\{z/x,y/c,f(b)/c\right\}} など無数に存在する。これらは本来の代入 { z / x , y / f ( b ) } {\displaystyle \left\{z/x,y/f(b)\right\}} に { x / a } {\displaystyle \left\{x/a\right\}} などの代入を合成したものなので、最汎単一化子 mgu は { z / x , y / f ( b ) } {\displaystyle \left\{z/x,y/f(b)\right\}} である。 一階述語論理での導出は mgu を用いて次のように表現できる。 もしリテラル L 1 ∈ C 1 {\displaystyle L_{1}\in C_{1}} と否定リテラル L 2 ¯ ∈ C 2 {\displaystyle {\overline {L_{2}}}\in C_{2}} が存在し、 L 1 {\displaystyle L_{1}} と L 2 {\displaystyle L_{2}} が mgu σ {\displaystyle \sigma } を持つ場合、以下の C R {\displaystyle C_{R}} が2項導出節（binary resolvent）である。ここで、 C 1 σ , C 2 σ {\displaystyle C_{1}\sigma ,C_{2}\sigma } などは、それぞれの節やリテラルに代入 σ {\displaystyle \sigma } を行ったものを表す。 C R = ( C 1 σ ∖ { L 1 σ } ) ∪ ( C 2 σ ∖ { L 2 σ ¯ } ) {\displaystyle C_{R}=(C_{1}\sigma \setminus \{L_{1}\sigma \})\cup (C_{2}\sigma \setminus \{{\overline {L_{2}\sigma }}\})} 同様のやり方での2以上の複数の節から同時に導出することも可能であり、超導出（hyper-resolution）と呼ばれる。
※この「一階述語論理での導出」の解説は、「導出原理」の解説の一部です。
「一階述語論理での導出」を含む「導出原理」の記事については、「導出原理」の概要を参照ください。
- 一階述語論理での導出のページへのリンク
