%0 Journal Article
%T 机器定理证明的反向归约方法
%A 李爱中？
%A 黄厚宽？
%A 乔佩利？
%J 软件学报
%P 354-359
%D 1996
%X 基于代数和递归函数理论，本文定义了代数递归谓词．代数递归谓词是一类广泛的谓词．基于数学归纳法，作者给出了证明代数递归谓词永真性的反向归约方法及相应的算法ｒｅｄｕｃｔｉｏｎ．由于采用反向归约方式来完成定理证明，从根本上消除了正向组合式定理证明所产生的组合爆炸，因而极大地提高了定理证明的效率．
%K 自动定理证明
%K 代数
%K 递归
%K 反向归约
%K 数学归纳法
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=19960605&flag=1