Logic and Computation Courses
Linear Arithmetic: Geometry, Algorithms, and Logic,
Dmitry Chistikov (University of Warwick, UK) and Christoph Haase (University of Oxford, UK)
Theories of linear arithmetic over R, Q, Z, and N are at the core of computational logic. Arising as generalizations of their existential conjunctive fragments-linear programming and integer programming-they occur in many contexts in computer science both in theory and practice. Reducing domain-specific constraints to a linear arithmetic theory is a standard and powerful problem-solving technique. Arithmetic theories are a fascinating object to study, as they lie at the interface of geometry, algorithmics, and logic. This course is an introduction to the theories of linear arithmetic, such as the first order linear theory of the reals and Presburger arithmetic, its analogue over the natural numbers. We will first explore the geometry of linear constraints over R and Z, defining convex polytopes and convex polyhedra, as well as so-called hybrid linear sets, their discrete analogue. Subsequently, we will cover classic algorithmic techniques for linear and integer programming (simplex method, interior-point methods, branch-and-bound and rounding techniques) and decision procedures for Presburger arithmetic, such as quantifier elimination and automata-based techniques. Finally, we will discuss applications of linear arithmetic theories in formal language theory and software verification.