In this paper we study the logical foundations of automated inductive theoremproving. To that aim we first develop a theoretical model that is centeredaround the difficulty of finding induction axioms which are sufficient forproving a goal. Based on this model, we then analyze the following aspects: the choice of aproof shape, the choice of an induction rule and the language of the inductionformula. In particular, using model-theoretic techniques, we clarify therelationship between notions of inductiveness that have been considered in theliterature on automated inductive theorem proving.
展开▼
