Presburger arithmetic and its extensions
Registration form: Register here
Course summary:Presburger arithmetic, or linear integer arithmetic (LIA), is a logic that allows one to express linear constraints on integers: equalities, inequalities, and divisibility by fixed nonzero integers. More formally, it is the first-order theory of integers with addition and ordering.
This short course will introduce Presburger arithmetic, discuss what can be expressed in this logical theory and its extensions, decision problems for them, and automated reasoning methods. No background knowledge in logic beyond Boolean connectives and quantifiers will be required.
Detailed course description:
The decision problem for Presburger arithmetic takes as input a sentence: a logical formula where all variables are "quantified away" (using quantifiers "for all" and "there exists"). The output is the truth value of the sentence, i.e., true or false.
Problems from a multitude of domains can be expressed in Presburger arithmetic. For example:
- The feasibility problem for integer programming (famously NP-complete) is a special case of the decision problem.
- The well-known Frobenius coin puzzle is another example, one in which quantifiers alternate.
- The Parikh theorem from automata theory shows that commutative images of context-free languages can also be expressed in Presburger arithmetic.
To determine whether a logical sentence is true or false, we can use algorithms. These build upon fundamental ideas such as the Fourier--Motzkin procedure for linear programming and Gaussian elimination for systems for linear equations. There are several software tools that implement algorithms for arithmetic theories (and Presburger arithmetic in particular), for instance so-called Satisfiability Modulo Theories (SMT) solvers.
In general, even the decidability of logical theories of arithmetic is not a given, because quantifiers range over infinite sets (Z or N for Presburger arithmetic). In this course, we will:
- Introduce Presburger arithmetic, logical theories of arithmetic more broadly, and decision problems for them.
- Show that Presburger arithmetic is decidable and prove lower and upper bounds for its computational complexity. Discuss three approaches to the design of algorithms for the decision problem.
- Study restrictions (fragments) of Presburger arithmetic that support more efficient decision procedures, e.g., existential Presburger arithmetic.
- Study extensions of Presburger arithmetic, e.g., with exponentiation, and discuss their decidability and computational complexity.
This is a beautiful area where algorithms, arithmetic, and logic come together, and with a multitude of directions to take (geometry, automata, symbolic computation, number theory, etc.).
About the lecturer:Dmitry Chistikov is an Associate Professor in the Department of Computer Science at the University of Warwick, United Kingdom.
His research interests lie in theoretical computer science, with a focus on the computational complexity of problems in automata theory and logic. He develops algorithms for such problems and determines under which conditions they are optimal.
Before joining Warwick in 2017, Chistikov held postdoctoral positions at Oxford and at the Max Planck Institute for Software Systems. He completed his PhD degree (Candidate of Sciences) in 2011 at Moscow State University.
With co-authors, Chistikov won a Distinguished Paper Award at LICS 2025 and a Best Paper Award at ICALP 2024.
Location and schedule:
|
|
|
||||||||||||||||