Proving Inductive Theorems Using Construction Bases

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.