王湘浩广义归结方法的推广 |
| |
引用本文: | 王元元.王湘浩广义归结方法的推广[J].军事通信技术,1985(2). |
| |
作者姓名: | 王元元 |
| |
摘 要: | 文献1]中王湘浩等给出了不同于 Robinson 归结方法的广义归结方法,可用于对不带等词的一阶谓词演算定理的一般形式直接进行机器证明。本文给出了不同于 Robinson 替换方法的广义替换方法,证明了广义替换方法与广义归结方法的联合使用,称为广义替换—归结方法,可对带等词的一阶谓词演算定理的一般形式直接进行机器证明,证明了广义替换—归结方法是合理的,完备的。
|
本文献已被 CNKI 等数据库收录! |
|