Advanced Reasoning in Arithmetic Theories

Arithmetic theories are logical theories for reasoning about number systems, such as the integers and reals. Such theories find a plethora of applications across computer science, including in algorithmic verification, artificial intelligence, and compiler optimisation. The appeal of arithmetic theories is their generality: once a problem has been formalised in a decidable such theory, a dedicated solver can in principle be used in a push-button fashion to obtain a solution. Arithmetic theories are also of great importance for showing decidability and complexity results in a variety of domains. Decision procedures for quantifier-free and linear fragments of arithmetic theories have been among the most intensively studied and impactful topics in theoretical computer science. However, emerging applications require more expressive theories, including support for quantifiers, counting, and non-linear functions. Unfortunately, the lack of understanding of the computational properties of such extensions means that existing decision procedures are not applicable or do not scale. The overall goal of this proposal is to advance the state-of-the-art in decision procedures for expressive arithmetic theories. To this end, starting with a recent breakthrough made by the PI, we will develop novel and optimal quantifier-elimination procedures for linear arithmetic theories, which we plan to eventually integrate into mainstream SMT solvers. Furthermore, we aim to improve complexity bounds and push the decidability frontier of extensions of arithmetic theories with counting and non-linear operations. The proposed research requires to tackle long-standing open problems---some of them being decades old. In short, the project will lay algorithmic foundations on which next-generation decision procedures and reasoners for arithmetic theories will be built.