11 August 2023
Linear Arithmetic Theories: Algorithms and Applications
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
EUR 490: Early student registration
EUR 690: Early non-academic registration
Scholarships
There are several scholarship options which you can read about on our website.