%0 Journal Article
%T 基于配对方法的自动定理证明
%A 陈玉泉？
%A 陆汝占？
%A 余皓？
%J 软件学报
%P 271-277
%D 1997
%X ｐｅｔｅｒｂ．ａｎｄｒｅｗｓ提出了自动定理证明的配对方法的理论和算法．本文针对该算法的缺点，给出了一个无需回溯的实现算法，并得到一个高阶逻辑的自动定理证明系统.
%K 自动定理证明
%K 配对
%K 归结
%K 关联
%K 高阶逻辑
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=19970405&flag=1