Automation of Logic

Arithmetic Reasoning

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.


Satisfiability Modulo Arithmetic and Theories (SMArT)

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.

Selected Publications

  1. M. Bromberger, T. Sturm, C. Weidenbach. Linear Integer Arithmetic Revisited. Accepted at CADE-25, 2015. Long version at arxiv:1503.02948.
  2. T. Sturm. Subtropical Real Root Finding. Accepted at ISSAC 2015. Preprint at arXiv:1501.04836.
  3. M. Košta, T. Sturm, A. Dolzmann. Better Answers to Real Questions. Accepted at Journal of Symbolic Computation, 2015. Preprint at arXiv:1501.05098.
  4. C. W. Brown, M. Košta. Constructing a Single Cell in Cylindrical Algebraic Decomposition. Journal of Symbolic Computation 70:14–48, 2015. doi:10.1016/j.jsc.2014.09.024.
  5. H. Errami, M. Eiswirth, D. Grigoriev, W. Seiler, T. Sturm, A. Weber. Detection of Hopf Bifurcations in Chemical Reaction Networks Using Convex Coordinates. Journal of Computational Physics 291:279–302, 2015. Open access at: doi:10.1016/j.jcp.2015.02.050.
  6. M. Košta, T. Sturm. A Generalized Framework for Virtual Substitution. 2015. arXiv:1501.05826.
  7. K. Korovin, M. Košta, T. Sturm. Towards Conflict-Driven Learning for Virtual Substitution. Proceedings of CASC 2014, LNCS 8660, 2014. doi:10.1007/978-3-319-10515-4_19.
  8. M. Košta. SMT-Based Compiler Support for Memory Access Optimization for Data-Parallel Languages. Proceedings of MACIS 2013, Nanning, China, December 11–13, 2013.
  9. N. Bjørner, R. Hähnle, T. Nipkow, C. Weidenbach (eds.). Deduction and Arithmetic. Dagstuhl Reports 3(10): 1–24, 2013.
  10. R. Karrenberg, M. Košta, T. Sturm. Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages. Proceedings of FroCoS 2013, LNAI 8152, 2013. doi:10.1007/978-3-642-40885-4_5.
  11. H. Errami, M. Eiswirth, D. Grigoriev, W. Seiler, T. Sturm, A. Weber. Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates. Proceedings of CASC 2013, LNCS 8136, 2013. doi:10.1007/978-3-319-02297-0_7.