Voigt, Marco Automation of Logic, MPI for Informatics, Max Planck Society;
Voigt, M. (2021). Decidable ∃∗∀∗ First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates. Journal of Automated Reasoning, 65, 357-423. doi:10.1007/s10817-020-09567-8.