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