Logical analysis of automated inductive theorem proving

Automating the search for proofs by induction is an imporant topic in computer science with a history that stretches back decades. A variety of different approaches and systems has been developed. Typically, these systems have been evaluated empirically and thus very little is known about their theoretical limitations.
In this talk I will show how to use mathematical logic to understand the theoretical power and limits of methods for automated inductive theorem proving. A central tool are translations of proof systems that are intended for automated proof search into (very) weak arithmetical theories. Thus unprovability results can be transferred from theories to methods of automated deduction.
I will describe concrete such analyses of two methods of automated inductive theorem proving including practically relevant unprovability results: 1. adding explicit induction axioms to a saturation theorem prover and 2. clause set cycles.
(Joint work with Jannik Vierling.)