Linear Arithmetic Theories: Algorithms and Applications

About

Arithmetic theories are logical theories for reasoning about number systems. They find several applications across computer science, including in verification, AI and compiler op- timisation. The foundations of arithmetic theories lie at the interface of logic, geometry and automata theory.
This course is an introduction to linear arithmetic theories, with an emphasis on Pres- burger arithmetic, the first-order theory of the integers with addition and order. We start by exploring the subject bottom up, introducing linear arithmetic theories with problems coming from optimisation and AI. Subsequently, we cover classic algorithms for linear and integer programming. The last three lectures focus on three algorithmic paradigms to decide Presburger arithmetic based on quantifier elimination, finite-state automata, and geometric decision procedures. We emphasise differences between these techniques by studying exten- sions of Presburger arithmetic that can be tackled in a natural way only within one of the three. We also demonstrate software offering support for these paradigms: RedLog (quan- tifier elimination), Walnut (finite-state automata), and SageMath (geometric procedures

Course leader

Alessio Mansutti and Christoph Haase

Target group

Students

Fee info