论文部分内容阅读
ＰｅｔｅｒＢ．Ａｎｄｒｅｗｓ提出了自动定理证明的配对方法的理论和算法．本文针对该算法的缺点，给出了一个无需回溯的实现算法，并得到一个高阶逻辑的自动定理证明系统
PeterB. Andrews proposed the theory and algorithm of the pairing method of automatic theorem proving. Aiming at the shortcomings of this algorithm, this paper gives a realization algorithm without backtracking and obtains a high-order logic automatic theorem proving system