# Some observations on the logical foundations of inductive theorem proving

## TL;DR

This paper explores the logical foundations of automated inductive theorem proving by developing a theoretical model to analyze the selection of induction axioms, proof shapes, rules, and formulas, clarifying their interrelations.

## Contribution

It introduces a new theoretical model centered on the difficulty of finding sufficient induction axioms and clarifies the relationships between different notions of inductiveness in the literature.

## Key findings

- Model highlights the importance of induction axiom selection
- Analysis of proof shape and induction rule choices
- Clarification of inductiveness notions via model-theoretic techniques

## Abstract

In this paper we study the logical foundations of automated inductive theorem proving. To that aim we first develop a theoretical model that is centered around the difficulty of finding induction axioms which are sufficient for proving a goal. Based on this model, we then analyze the following aspects: the choice of a proof shape, the choice of an induction rule and the language of the induction formula. In particular, using model-theoretic techniques, we clarify the relationship between notions of inductiveness that have been considered in the literature on automated inductive theorem proving. This is a corrected version of the paper arXiv:1704.01930v5 published originally on Nov.~16, 2017.