R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

L. Bachmair, H. Ganzinger, and U. Waldmann, Refutational theorem proving for hierarchic first-order theories, Applicable Algebra in Engineering, Communication and Computing, vol.1, issue.3-4, pp.193-212, 1994.
DOI : 10.1007/BF01190829

P. Baumgartner and U. Waldmann, Hierarchic Superposition with Weak Abstraction, Automated Deduction (CADE-24), pp.39-57, 2013.
DOI : 10.1007/978-3-642-38574-2_3

URL : https://hal.archives-ouvertes.fr/hal-00931919

A. R. Bradley, Z. Manna, and H. B. Sipma, What???s Decidable About Arrays?, Verification, Model Checking, and Abstract Interpretation (VMCAI'06), pp.427-442, 2006.
DOI : 10.1007/11609773_28

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

J. Peter and . Downey, Undecidability of Presburger Arithmetic with a Single Monadic Predicate Letter, 1972.

A. Fietzke and C. Weidenbach, Superposition as a Decision Procedure for Timed Automata, Mathematics in Computer Science, vol.6, issue.1, pp.409-425, 2012.
DOI : 10.1007/s10009-003-0135-4

Y. Ge and L. Mendonça-de-moura, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification (CAV'09), pp.306-320, 2009.
DOI : 10.1007/978-3-540-78800-3_19

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

M. Horbach, M. Voigt, and C. Weidenbach, On the Combination of the Bernays?Schönfinkel?Ramsey Fragment with Simple Linear Integer Arithmetic, Automated Deduction (CADE-26

M. Horbach, M. Voigt, and C. Weidenbach, The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable, ArXiv preprint, p.2017
URL : https://hal.archives-ouvertes.fr/hal-01592177

D. Kroening and O. Strichman, Decision Procedures. Texts in Theoretical Computer Science. An EATCS Series, 2016.

E. Kruglov and C. Weidenbach, Superposition Decides the First-Order Logic Fragment Over Ground Theories, Mathematics in Computer Science, vol.3, issue.3???4, pp.427-456, 2012.
DOI : 10.1016/B978-044450813-3/50029-1

P. Niebert, M. Mahfoudh, E. Asarin, M. Bozga, O. Maler et al., Verification of Timed Automata via Satisfiability Checking, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'02), pp.225-244, 2002.
DOI : 10.1007/3-540-45739-9_15

URL : https://hal.archives-ouvertes.fr/hal-00374806

R. Vaughan and . Pratt, Two Easy Theories Whose Combination is Hard, Massachusetts Institute of Technology, 1977.

H. Putnam, Decidability and essential undecidability, The Journal of Symbolic Logic, vol.17, issue.01, pp.39-54, 1957.
DOI : 10.1007/BF01443610

M. Voigt, The Bernays?Schönfinkel?Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable, ArXiv preprint, p.2017

M. Voigt and C. Weidenbach, Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete, ArXiv preprint, p.2015