| 摘要: |
| 基于代数和递归函数理论，本文定义了代数递归谓词．代数递归谓词是一类广泛的谓词．基于数学归纳法，作者给出了证明代数递归谓词永真性的反向归约方法及相应的算法Ｒｅｄｕｃｔｉｏｎ．由于采用反向归约方式来完成定理证明，从根本上消除了正向组合式定理证明所产生的组合爆炸，因而极大地提高了定理证明的效率． |
| 关键词: 自动定理证明 代数 递归 反向归约 数学归纳法 |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家自然科学基金资助. |
|
| BACKWARD REDUCTION METHOD FOR AUTOMATED THEOREM PROVING |
|
Li Aizhong,Huang Houkuan,Qiao Peili
|
| Abstract: |
| Based on algebra and recursive function theory, a key concept of algebraicrecursive predicates is defined in this paper. Based on mathematical induction, a backwardreduction method and its corresponding algorithm reduction are given for proving the universal truth of algebraic recursive predicates. Because the method is reduction based, theefficiency of theorem-proving is improved greatly. |
| Key words: Automated theorem proving algebra recursion backward reduction mathematical induction. |
