Logical Theories of Arithmetic are formal frameworks used to study numbers, their properties, and related arithmetic operations using logical reasoning. Examples include Presburger Arithmetic, first-order theory of natural numbers with addition and order, and Peano Arithmetic, which encompasses both addition and multiplication, along with the order predicate. These theories are foundational in mathematics and computer science, with applications raging from automated reasoning to verification. The workshop on "Recent Developments on Arithmetic Theories and Applications" aims to bring together researchers to explore recent advances in the field. By fostering discussions on recent results, the event seeks to promote collaborative research in the area of First-Order (and higher-order) Arithmetical theories while inspiring young researchers to contribute to this field. This workshop is a satellite event of 11th Indian Conference of Logic and Its Applications (ICLA, 2025).
Abstract: In [Pacific J. Math., 16(2), 1966] Ginsburg and Spanier established
a fundamental result regarding the geometry of the solutions
of a Presburger arithmetic formula. A set is definable in
Presburger arithmetic if and only if it is semilinear.
The importance of this result is not only theoretical:
several applications stemming from program verification
and compiler optimization require reasoning
on the set of solutions of a Presburger arithmetic formula.
For these applications, semilinear sets are the right tool.
To show the left to right implication of their result,
Ginsburg and Spanier argued as follows:
-set of solutions of any system of linear
inequalities over the integers is semilinear
-semilinear sets are closed under union, projection
and complementation.
These facts directly give a "geometric procedure" that,
given a Presburger arithmetic formula, computes a semilinear
set representing all its solutions.
Following the result of Ginsburg and Spanier, several
authors tried to improve the geometric procedure to
make it as efficient as the other decision procedures
for Presburger arithmetic (which are based on
quantifier elimination or automata). See e.g. [Huynh,
ICALP'80], [Chistikov and Haase, ICALP'16] and [Beier
et al., AFL'17] for a few papers on this issue. The
crucial problem turned out to be the definition of an
optimal algorithm for the complementation of a
semilinear set, which stood open for a few decades.
In 2022, Dmitry Chistikov, Christoph Haase and I
discovered such an algorithm, and in this talk I will
describe some of its core steps. Surprisingly,
from properties of the semilinear sets computed following
our procedure, we can also answer a conjecture of
D. Nguyen and I. Pak [Combinatorica 39, pp. 923–932, 2019]
on the hardness of PAC learning Presburger formulae.
In particular, we find that the Vapnik–Chervonenkis (VC) dimension
of a Presburger arithmetic formula is at most doubly exponential
in the size of the formula; and this bound is tight for an infinite
family of formulae.
This talk is based on the paper "Geometric decision
procedures and the VC dimension of linear arithmetic
theories" [Chistikov, Haase, Mansutti, 59, LICS'22].
Abstract: In the early 1960s, R. J. Büchi made a fundamental discovery: decidability of arithmetic theories can be established using automata theory. Moreover, the exact expressive power of finite automata can be described via an extension of Presburger arithmetic, which is now known as Büchi arithmetic. The nature of this theory is radically different from the well-studied Presburger arithmetic, and for this reason the classical questions of complexity and expressivity for Büchi arithmetic remained unsolved for a long time.
In my talk, I will first give a sketch of the proof of the Büchi's theorem and then show the relationships between Büchi arithmetic and the integer arithmetic of addition and usual bitwise operations NOT, AND, OR.
Next, I will show why the quantifier-elimination approach, which is not applicable to prove decidability of Büchi arithmetic, becomes a powerful tool for studying the expressive power of its existential fragment.
Finally, it will be shown that the developed quantifier-elimination techniques can be combined with the decision procedure for Presburger arithmetic with the base 2 exponentiation. This combination provides a new algorithm for the integer linear-exponential programming feasibility, which was (before 2024) only known to be decidable in exponential space using a purely automata-theoretic procedure. In contrast, the quantifier-elimination procedure runs in non-deterministic polynomial time.
Abstract: In a separability problem, we are given two sets K and L from a class C, and we want to decide whether there exists a set R from a class S such that K ⊆ R and R ∩ L = ∅. In this case, we speak of separability of sets in C by sets in S. This problem has applications in safety verification: it can be used to certify the disjointness of the reachable configurations in a program with a set of undesired states.
We study two types of separability problems. First, we consider separability of Presburger definable sets, i.e. semilinear sets, by sets definable by quantifier-free monadic Presburger formulas (or equivalently, the recognizable subsets of ℕ^d). Here, a formula is monadic if each atom uses at most one variable. Second, we consider separability of languages of Parikh automata by regular languages. A Parikh automaton is a machine with access to counters that can only be incremented, and have to meet a semilinear constraint at the end of the run. Both of these separability problems are known to be decidable with elementary complexity.
Our main results are that both problems are coNP-complete. In the case of semilinear sets, coNP-completeness holds regardless of whether the input sets are specified by existential Presburger formulas, quantifier-free formulas, or semilinear representations. Our results imply that recognizable separability of rational subsets of Σ^* × ℕ^d (shown decidable by Choffrut and Grigorieff) is coNP-complete as well. Another application is that regularity of deterministic Parikh automata (where the target set is specified using a quantifier-free Presburger formula) is coNP-complete as well.
Abstract: Sturmian words are the simplest non-periodic words: a word w of zeros and ones is Sturmian if for every n, the number of distinct factors of w of length n is exactly n+1. I will discuss recent applications of Sturmian and other special classes of words (e.g. billiard words) with rich combinatorics to automatic structures, focussing on two results: the monadic second-order theory of natural numbers expanded with two power predicates (e.g. powers of two and powers of three) is decidable and the first-order theory of Presburger arithmetic expanded with two power predicates is undecidable for already formulas with three alternating blocks of quantifiers.
Date: February 1, 2025
Venue: ISI Kolkata
| Time | Event | Speaker |
|---|---|---|
| 09:30 - 09:45 | Opening Remarks/Introduction | |
| 09:45 - 10:30 | Büchi Arithmetic: Finite Automata and Quantifier Elimination | Mikhail R. Starchak |
| 10:30 - 11:00 | Coffee Break | - |
| 11:00 - 11:45 | From Word Combinatorics to Automatic Structures | Toghrul Karimov |
| 11:45 - 12:30 | The Separability Problem for Presburger Definable Sets and Parikh Automata | Chris Köcher |
| 12:35 - 13:05 | An optimal geometric procedure for Presburger arithmetic | Alessio Mansutti |
| 13:05 - 13:10 | Closing Remarks |
For more information, please reach out to us at kmadnani@mpi-sws.org.