用构造基证明归纳定理
Proving Inductive Theorems Using Construction Bases
-
摘要: 在测试集方法的基础,引入一个新的概念-构造基,用于产生完全的但非冗余的不可归的约基项;提出构造基归纳原理,将显式归纳证明和隐式归纳证明有机地结合在一起。对测试集方法做出了改进,实验表明:这种方法提高了归纳定理的证明效率。Abstract: On the basis of test set approach we present a new concept, construction base, that is used to produe complete and irredundant irreducible ground terms, and put forward a construction base induction principle, which organically combines explicit induction and implicit induction and improves test set methods. experimental results show that: our method is more efficient to prove inductive theorems.