Automated Reasoning for Numerical Analysis

Proving in numerical analysis usually requires both ingenuity and technical proficiency (e.g., in matrix calculus). The goal of the thesis will be to free researchers in numerical analysis from some of the more technical aspects of proving, allowing them to concentrate on the creative aspects of their work. The thesis work will start with an analysis of several important articles in the field of numerical analysis. Based on this, we will identify relevant techniques from automated reasoning and, based on that, build a tool for supporting researchers in their everyday proof work.