论文部分内容阅读
文献[1]中王湘浩等给出了不同于 Robinson 归结方法的广义归结方法,可用于对不带等词的一阶谓词演算定理的一般形式直接进行机器证明。本文给出了不同于 Robinson 替换方法的广义替换方法,证明了广义替换方法与广义归结方法的联合使用,称为广义替换—归结方法,可对带等词的一阶谓词演算定理的一般形式直接进行机器证明,证明了广义替换—归结方法是合理的,完备的。
Wang Xianghao et al [1] give a generalized reduction method different from the Robinson reduction method, which can be used to directly prove the general form of first-order predicate calculus theorems without terms. In this paper, we give a generalized substitution method that is different from Robinson’s substitution method, and prove that the combination of generalized substitution method and generalized reduction method, called generalized substitution-reduction method, can directly measure the general form of the first-order predicate calculation theorem Prove the machine, proved that the generalized replacement - the method of summary is reasonable and complete.