The limits of automated inductive theorem provers

Abstract

In this thesis we formally analyze the limits of several saturation-based inductive theorem provers. We propose an analysis technique that consists in reducing provers into first-order theories with induction. At first sight the reduction of a prover into a first-order theory may seem to be a very strong abstraction. Therefore, it is a priori not clear whether such reductions retain some useful information about the original prover. In this thesis we show that this approach permits to extract crucial logical features and provides strong bounds on the logical strength of provers. Moreover, based on these bounds, we prove various unprovability results, whereas previously only empirical observations could be made based on the failure of concrete implementations. The unprovability results in this thesis show that, despite the loss of details incurred by the reduction of a prover to a first-order theory, there are elementary properties that are not provable by recent automated inductive theorem provers even given any amount of time and memory. Furthermore, the thesis links these unprovability results to a certain extent to the logical features of the provers and thus provides some guidance for the development of more powerful automated inductive theorem provers.