王湘浩广义归结方法的推广

文献1]中王湘浩等给出了不同于 Robinson 归结方法的广义归结方法,可用于对不带等词的一阶谓词演算定理的一般形式直接进行机器证明。本文给出了不同于 Robinson 替换方法的广义替换方法,证明了广义替换方法与广义归结方法的联合使用,称为广义替换—归结方法,可对带等词的一阶谓词演算定理的一般形式直接进行机器证明,证明了广义替换—归结方法是合理的,完备的。