关于归纳证明的探讨

Studies in Proof by Induction

归纳定理证明是一种难度较大且较有前途的一种自动定理证明方法。较早的归纳定理证明器是Boyer一Moore于1979年提出的BM证明器,BM证明器采用的是传统的结构归纳法,对所证公式中的每个函数项都根据其所谓归纳模板提出相应的归纳方案,然后对这个归纳方案进行分析、比较和整理。

Automatic proofs in theories is a major field of study in computer science and artificial intelligence . and proof by induction is one of the most important and promising automatic proofs in theories. The paper introduces and studies some of the approaches and methods for proof by induction in theories.