Reasoning about problems expressible in arithmetic has been one of the most prominent applications of computer science since the early days. This Dagstuhl Seminar aims to bring together academic and industrial researchers working on the theory and practice of arithmetic reasoning, with a focus on the following areas:

• Computer Algebra
• Formal Methods
• Logical Aspects of Arithmetic
• Mathematical Optimization
• Satisfiability Modulo Theories

Perhaps for historical reasons, despite significant advances in all of these areas, interaction between them has been limited. The goal of this Dagstuhl Seminar is to establish a bridge between different communities working on different aspects of arithmetic, to enable rapid knowledge exchange, the identification of cross-community challenges, and to lay the foundation for sustained interaction beyond the seminar.

The program of the seminar will feature a combination of:

1. Presentations and lectures by experts from the various areas, designed to introduce all participants to the distinct perspectives the various communities offer on arithmetic reasoning. These will touch upon new developments such as foundational results, algorithms, faster decision procedures, new software libraries and tools, novel application domains, etc.
2. Discussions on critical topics in these areas. These topics include the limitations of current algorithmic techniques, unresolved problems in arithmetic reasoning, and challenges in tool development (such as standardization efforts and the creation of benchmark suites).
3. Technology transfer. These sessions will focus on the better understanding of mutual expectations between theoreticians and researchers developing tools. What are the challenges faced when implementing and optimizing “pen and paper” algorithms? What properties should tools have to facilitate academic experimentation?
4. Time for collaboration, to explore shared interests and challenges, and find promising research directions that will, in a tangible way, bring the communities closer. Non-scientific collaboration will also be encouraged, such as the development of action plans for further enhancing the connections among the various research areas.

Creative Commons BY 4.0

Erika Abraham, Dmitry Chistikov, Christoph Haase, Matthias Köppe, and Alessio Mansutti