Pure mathematics

Discrete mathematics

Theoretical computer science

Computer science

Decidability

Peano axioms

Presburger arithmetic

Mathematics

Programming language

Second-order arithmetic

Algebra over a field

Arithmetic

ACM SIGLOG News

The first-order theory of the integers with addition and order, commonly known as Presburger arithmetic, has been a central topic in mathematical logic and computer science for almost 90 years. Presburger arithmetic has been the starting point for numerous lines of research in automata theory, model theory and discrete geometry. In formal verification, Presburger arithmetic is the first-choice logic to represent and reason about systems with infinitely many states. This article provides a broad yet concise overview over the history, decision procedures, extensions and geometric properties of Presburger arithmetic.

A survival guide to presburger arithmetic