November 7
Stefan Hetzl,
Vienna University of Technology
Arithmetical theories and the automation of induction
This talk is about the relationship between (weak) arithmetical theories and methods for automated inductive theorem proving. Automating the search for proofs by induction is an important topic in computer science with a history that stretches back decades. A variety of different approaches, algorithms and implementations has been developed.
In this talk I will present a logical approach for understanding the 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 weak arithmetical theories. Another central tool are non-standard models of these weak arithmetical theories.
This approach allows to obtain independence results which are of practical interest in computer science. It also gives rise to a number of new problems and questions about weak arithmetical theories.