ARiAT - Advance Reasoning in Arithmetic Theories

The aim of the ARiAT project is to break new ground in the field of 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 project is to advance the state of the art in decision procedures for expressive arithmetic theories. To this end, the project will develop novel and optimal quantifier-elimination procedures for linear arithmetic theories, which will be eventually integrated into mainstream SMT solvers. Furthermore, it aims to improve complexity bounds and push the decidability frontier of extensions of arithmetic theories with counting and non-linear operations. The proposed research requires the tackling of long-standing open problems - some of which are decades old. The project will lay algorithmic foundations on which next-generation decision procedures and reasoners for arithmetic theories will be built.