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.

ARiAT is generously supported by the European Research Council

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.

Avatar
Christoph Haase
Associate Professor