Room 206 (2nd floor, badged access)
7 décembre 2021 - 14h00
Efficient complementation of semilinear sets and the VC dimension of Presburger arithmetic
par Alessio Mansutti de University of Oxford
Abstract: We discuss the issue of deciding the first-order theory of integer linear arithmetic, also known as Presburger arithmetic.
Whereas optimal decision procedures based on either quantifier-elimination or automata constructions are known for this theory,
the current procedures based on manipulating semilinear sets (i.e. sets that geometrically characterise the solutions of a formula)
are extremely inefficient. We address this issue by deriving a new algorithm for computing the complement of a semilinear set,
which in particular is optimal for nested complementations. Alongside solving the aforementioned discrepancy between semilinear-based
algorithms and other types of procedures, this result allows us to characterise the Vapnik-Chervonenkis dimension of Presburger arithmetic,
which is found to be doubly-exponential. The results in this talk are joint work with Christoph Haase and Dmitry Chistikov.
