Trends in Arithmetic Theories 2024

About

Logical theories of arithmetic such as Presburger arithmetic play an important role in a variety of different areas of computer science and have been studied since the early days of the field. The recent years have seen a lot of progress on all aspects of such theories, ranging from new foundational results, algorithmic advances, more performant decision procedures to novel application domains. This progress has largely been obtained independently without much interaction between researchers working on different aspects of this field. The goal of this workshop is to bring together researchers working in the field to exchange latest trends, understand currently existing challenges and to initiate new collaborations.

Everyone interested in arithmetic theories is invited to attend.

Invited speakers

• Olivier Bournez, École Polytechnique, France
  Invited talk: Characterisations of polynomial-time and -space complexity classes using (discrete) ordinary differential equations
  Several recent works have studied how analogue models of computation compare to classical digital ones. By “analog” models of computation, we mean computing over continuous quantities, while “digital” models work on discrete structures, like bits. It led to a broader use of Ordinary Differential Equation (ODE) in computation theory. From this point of view, the field of implicit complexity has also been widely studied and developed. Using arguments from computation theory and computable analysis, we show that we can algebraically characterise PTIME and PSPACE for functions over the integers and even over the reals. This leads to ways to characterise classical complexity classes using schemas based on arithmetic and finite differences (discrete ODEs). This also shows how we can program, even over the discrete, using changes of variables controlled by dynamics such as linear ODEs.
• Sławomir Lasota, Univ. Warsaw, Poland
  Invited tutorial: Orbit-finite linear programming
  An infinite set is orbit-finite if, up to permutations of atoms, it has only finitely many elements. Orbit-finite sets admit finite presentations that can be input to algorithms. The lecture is devoted to a generalisation of linear programming where constraints are expressed by an orbit-finite system of linear inequalities. I will present a procedure for checking if such a system has a real solution, and for computing the minimal/maximal value of a linear objective function over the solution set. When the parameter called ‘atom dimension’ is fixed, the procedure works in polynomial time. Thus the complexity of orbit-finite linear programming matches the complexity of classical finite one. In sharp contrast to this positive result, orbit-finite integer linear programming (where only integer solutions are sought) is undecidable.
• Alessio Mansutti, IMDEA, Spain
  Invited tutorial: Existential Presburger Arithmetic with Divisibility Constraints: A tour
  In the 1970s, Leonard Lipshitz established a surprising result: while there is no algorithm for solving A system of polynomial equations (Hilbert’s 10th problem), adding to the existential fragment of Presburger arithmetic a divisibility predicate between linear polynomials results in a decidable theory. Very recently, this theory, commonly referred to as EPAD (acronym for Existential Presburger Arithmetic with Divisibility), has found applications to problems stemming from word equations and automata theory. Because of these applications, the exact complexity of the satisfiability problem for EPAD is nowadays considered a fundamental open problem in arithmetic theories. It is known to lie in NEXPTIME, but no lower bound other than an NP-hardness result for the 2 variables fragment is known.

  The aim of this tutorial is to given an introduction to EPAD. The tutorial is split into three parts. In the first part, we familiarise with EPAD by looking at properties expressible in the logic, ultimately giving an NP-hardness proof for its fragment of formulae consisting of 2 variables and 6 constraints. We also give a brief overview of some of the applications that EPAD has in the context of word equations and automata theory. In the second part, we study (with a reasonable level of details) Lipshitz’s algorithm for solving EPAD formulae. If time permits, in the third part of the tutorial we discuss a few recent improvements on Lipshitz’s procedure, and interesting corollaries of these improvements.

  The tutorial is based on the following papers:

  • Leonard Lipshitz. “The Diophantine problem for addition and divisibility”. Trans. Am. Math. Soc, 1978.
  • Leonard Lipshitz. “Some remarks on the Diophantine problem for addition and divisibility”. Bull. Soc. Math. Belg. Sér. B, 1981.
  • Antonia Lechner, Joël Ouaknine, and James Worrell. “On the complexity of linear arithmetic with divisibility”. LICS’15.
  • Florent Guépin, Christoph Haase, and James Worrell. “On the existential theories of Büchi arithmetic and linear p-adic fields”. LICS’19.
  • Rémy Défossez, Christoph Haase, Alessio Mansutti and Guillermo A. Pérez. “Integer Programming with GCD Constraints”. SODA’24.
• Joris Nieuwveld, MPI-SWS, Germany
  Invited talk: Logical theories combined with multiple powers
  Since the time of Büchi, there has been significant work on adding powers of a natural number to logical theories like Presburger arithmetic, both as functions and predicates. Examples of such theories are Büchi Arithmetic and Semënov Arithmetic. More recently, interest has grown into adding multiple powers at once. For example, Hieronymi and Schultz showed that Presburger arithmetic becomes undecidable when adding the powers of two and three. In this talk, I will discuss positive results in this direction. Notably, it turns out that monadic second-order logic (MSO) over the natural numbers remains decidable when adding the powers of two and three as predicates. Moreover, assuming Schanuel’s Conjecture, decidability is maintained even when adding arbitrarily many predicates coming from powers of natural numbers. Next, I will share recent work on the existential fragment of the theory that Hieronymi and Schultz proved to be undecidable. During this talk, I will discuss the number-theoretical methods used and the number-theoretical barriers one has to overcome when trying to extend these results. sc
• Žaneta Semanišinová, TU Dresden, Germany
  Invited talk: Identifying Tractable Quantified Temporal Constraints
  The constraint satisfaction problem, parameterized by a relational structure, provides a general framework for expressing computational decision problems. An important class of templates used in this context are temporal structures, i.e., structures first-order definable over (Q; <). In the standard setting, which allows only existential quantification over input variables, the complexity of temporal constraints has been fully classified. In the quantified setting, i.e., when one also allows universal quantifiers, there is only a handful of partial classification results and many concrete cases of unknown complexity. In this talk we present significant progress towards understanding the complexity of the quantified constraint satisfaction problem (QCSP) for temporal structures. We provide a complexity dichotomy for quantified constraints over the Ord-Horn fragment, showing that all problems under consideration are in P or coNP-hard. In particular, we determine the complexity of QCSP(Q; x=y⇒x≥z), hereby settling a question open for more than ten years.

  This is joint work with Jakub Rydval and Michał Wrona.

Click on the triangle below the talk title to view the abstracts.

Timetable

The workshop follows the joint workshop schedule for ICALP’24 satellite workshops. All times are in in local time (EEST (UTC+3)).

09:05 – 09:15   Opening
09:15 – 10:00   Olivier Bournez
10:00 – 10:30   Coffee break
10:30 – 12:00   Tutorial: Alessio Mansutti
12:00 – 12:45   Žaneta Semanišinová
12:45 – 14:00   Lunch
14:00 – 15:30   Tutorial: Sławomir Lasota
15:30 – 16:00   Coffee break
16:00 – 16:45   Joris Nieuwveld

Registration

The registration is handled via the main ICALP registration.

Local information

TBC

Organisation

Dmitry Chistikov (Univ. Warwick)
Christoph Haase (Univ. Oxford)
Radek Piórkowski (Univ. Oxford)

Acknowledgements

This workshop receives support through the ERC project ARiAT.