返回主页

   一般子句的归结

     为将归结原理应用于含有变量的子句 ，应找出一个置换，作用于给定的两个子句，使它们包括互补的文字。为方便起见，首先将两个给定的子句表示成两个文字的集合{L_i}和{M_i}，并假设两个子句的变量符号是不同的，令{l_i}是{L_i}的一个子集，{m_i}是{M_i}的一个子集。设s是集合{l_i}和{Øm_i}的并集的最简合一者，则由 {L_i}和{M_i}可以得到它们的归结式

    {{L_i}-{l_i}}s∨{{M_i}-{m_i}}s

        当两个子句作归结式，子集 {l_i}和{m_i}的选取可能有多种形式，因此得到的归结式也不是唯一的。例如考虑子句

    P[x,f(A)]∨P[x,f(y)]∨Q(y)

和

    ØP[z,f(y)]∨ØQ(z)

如果取{l_i}={P[x,f(A)]}和m_i={ØP[z,f(A)]}，则它们的最简合一者为s={z/x}，得到的归结式

         P[z,f(y)]∨ØQ(z)

如果取{l_i}={P[x,f(A)]}和m_i={ØP[z,f(y)]}，则它们的最简合一者为s={z/x,A/y}，得到的归结式 

　       Q(y)∨ØQ(z)

                             返回