ARiAT is a research project investigating decision procedures for arithmetic theories supported by the European Research Council with an ERC Starting Grant. The project started in January 2020 and runs over a period of five years.

At a glance

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, starting with recent breakthroughs [CH16, CH17, HZ19, GHW19], 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.

Trends in Arithmetic Theories Workshop

Another goal of this project is to organise an annual workshop on Trends in Arithmetic Theories co-located with major conferences in theoretical computer science and verification. Since progress in the diverse area of arithmetic theories has largely been obtained independently without much interaction between researchers working on different aspects of this field, the goal of this workshop series is to bring together researchers to exchange latest trends, understand currently existing challenges and to initiate new collaborations. Due to the COVID-19 pandemic, the workshop did not take place during the first two years of the project.

So far, the following workshops have taken place:

• 1st Trends in Arithmetic Theories workshop held in Paris 4 July 2022