Arithmetic theories are first-order logics about number systems, such as the integers or the real numbers. They represent a fundamental branch in mathematical logic, and play a pivotal role in various areas of computer science. Their applications span both theoretical and practical domains, including control theory, mechanical engineering, compiler optimization, and program verification.

This talk overviews my recent work on designing procedures for arithmetic theories featuring non-linear functions such as exponentiation and trigonometric functions. As we will see, handling these functions comes at the cost of abandoning many of the fundamental properties of (integer) linear programming, to the point that even the seemingly straightforward task of encoding solutions becomes challenging. We will explore how to circumvent these problems, obtaining efficient algorithms (in theory and/or in practice).

The talk is based on the current progress and future objectives of my Marie-Curie Fellowship.