Arithmetic reasoning covers the study of first-order logic and arithmetic in theory and practice. In our work we focus on the design of new and the extension and optimization of existing arithmetic reasoning procedures as well as on their application in problems from various scientific disciplines like chemistry, systems biology and physics.

In the heart of our work lies the realization of the theoretical research as state-of-the art implementations in Redlog, a computer logic system based on the computer algebra system Reduce, and as stand-alone C applications, designed with the goal to be eventually migrated into the first-order superposition solver Spass.

Recent results include advancements in quantifier elimination procedures over the reals, compiler optimization, linear integer programs in verification systems and theory-solving via superposition. In ongoing research, we aim to further extend the applicability of the methods in automated reasoning and of our implementations.

The SMArT project, funded by ANR and DFG within the Programme Blanc, aims at providing new solutions in the field of satisfiability modulo theories (SMT) in combination with non-linear arithmetic. The focus of the project lies on both, new theoretical insights as well as a state-of-the-art software implementations. These ideas are put into practice by a multilateral cooperation between several groups including established research teams and industrial partners. Pascal Fontaine and his team at Inria/Loria in Nancy, France, are the designers of the award-winning SMT-solver veriT. The non-linear arithmetic facilities for veriT are provided by our researchers in Saarbrücken under the supervision of Thomas Sturm, co-developer of one of the most mature computer logic systems, Redlog. Additional support is given by researchers at DIMAp/UFRN, Natal, Brazil and our industrial partner Systerel, Aix-en-Provence, France, that allows us to direct our developement towards real-world application scenarios.