一个用于一阶逻辑（FOPC）自动定理证明的新算法
-
1陈勇浩.一个用于一阶逻辑自动定理证明的新算法[J].计算机工程与科学,1993,15(3):1-9.
-
2陈玉泉,陆汝占,余皓.基于配对方法的自动定理证明[J].软件学报,1997,8(4):271-277. 被引量：1
-
3刘全,孙吉贵.基于语义tableau的一阶逻辑自动定理证明[J].计算机工程与应用,2005,41(23):22-24. 被引量：3
-
4缪淮扣,吴茂康.自动定理证明中带有等词的连接法[J].应用科学学报,1994,12(3):246-252.
-
5汪娟,李兆鹏,陈意云.支持用户自定义谓词的自动定理证明的研究[J].小型微型计算机系统,2013,34(8):1781-1786.
-
6贲可荣,陈火旺.自动定理证明:十年回顾[J].计算机科学,1993,20(4):19-23. 被引量：1
-
7钟发荣,孙永强.关于归纳证明的探讨[J].计算机科学,1998,25(5):59-61.
-
8刘叙华,孙吉贵.相关逻辑L_5系统的Curry性质[J].中国科学（A辑）,1993,23(12):1320-1325.
-
9缪淮扣,李迎豪,吴茂康.COMPS连接法定理证明系统[J].计算机工程,1993,19(3):38-43.
-
10张健.基于重写技术的自动定理证明[J].计算机科学,1992,19(2):79-80.
;
