On the existential fragment of Büchi arithmetic

Christoph Haase
University College London
Thursday, 18 June, 2020 - 14:00
Zoom (Online)

Büchi arithmetic is an extension of Presburger arithmetic, the first-order theory of the natural numbers with addition. For a fixed base p, Büchi arithmetic additionally includes a binary predicate V_p such that V_p(x,y) holds if x is the largest power of p dividing y without remainder. Büchi arithmetic has been studied over the last 60 years and has led to deep theorems such as the Cobham-Semenov which states that if a set S of natural numbers is definable in Büchi arithmetic with respect to two multiplicatively independent bases then S is definable in Presburger arithmetic. However, the computational complexity of Büchi arithmetic has received suprisingly little attention. While it has been known that the full first-order theory of Büchi arithmetic has non-elementary time complexity, the computational complexity of its existential fragment has been open for over 30 years. In this talk, I will show that existential Büchi arithmetic is NP-complete, just like the existential fragment of Presburger arithmetic. In contrast to the latter, solutions sizes for formulas of existential Büchi arithmetic grow super-polynomially which poses a challenge for showing membership in NP. I will conclude the talk with a discussion on some open problems.