E. Althaus, E. Kruglov, and C. Weidenbach, Superposition Modulo Linear Arithmetic SUP(LA), Frontiers of Combining Systems (FroCoS'09), pp.84-99, 2009.
DOI : 10.1016/B978-044450813-3/50029-1
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.452.5808

R. Alur and T. A. Henzinger, A really temporal logic, Journal of the ACM, vol.41, issue.1, pp.181-204, 1994.
DOI : 10.1145/174644.174651

A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz, New results on rewrite-based satisfiability procedures, ACM Transactions on Computational Logic, vol.10, issue.1, 2009.
DOI : 10.1145/1459010.1459014
URL : https://hal.archives-ouvertes.fr/inria-00576862

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, pp.39-57, 2013.
DOI : 10.1007/978-3-642-38574-2_3
URL : https://hal.archives-ouvertes.fr/hal-00931919

N. Bjørner, K. L. Mcmillan, and A. Rybalchenko, On Solving Universally Quantified Horn Clauses, Static Analysis (SAS'13), pp.105-125, 2013.
DOI : 10.1007/978-3-642-38856-9_8

E. Börger, E. Grädel, and Y. Gurevich, The Classical Decision Problem, Perspectives in Mathematical Logic, 1997.
DOI : 10.1007/978-3-642-59207-2

A. R. Bradley, Safety Analysis of Systems, 2007.

R. Aaron, Z. Bradley, and . Manna, The Calculus of Computation, 2007.

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=10.1.1.119.4969

R. E. Bryant, S. K. Lahiri, and S. A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Computer Aided Verification (CAV'02), pp.78-92, 2002.
DOI : 10.1007/3-540-45657-0_7

D. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005.
DOI : 10.1145/1066100.1066102
URL : http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.70.1745&rep=rep1&type=pdf

J. Peter and . Downey, Undecidability of presburger arithmetic with a single monadic predicate letter, 1972.

B. Herbert and . Enderton, A mathematical introduction to logic, 2001.

M. Fischer and M. O. Rabin, Super-Exponential Complexity of Presburger Arithmetic, SIAM-AMS Symposium in Applied Mathematics, pp.27-41, 1974.
DOI : 10.1007/978-3-7091-9459-1_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.9759

C. Flanagan, R. Joshi, and J. B. Saxe, An explicating theorem prover for quantified formulas, 2004.

H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, DPLL(T): Fast Decision Procedures, Computer Aided Verification (CAV'04), pp.175-188, 2004.
DOI : 10.1007/978-3-540-27813-9_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.8015

S. Garfunkel and J. H. Schmerl, The undecidability of theories of groupoids with an extra predicate, Proceedings of the, pp.286-289, 1974.
DOI : 10.1090/S0002-9939-1974-0325378-3

Y. Ge, C. W. Barrett, and C. Tinelli, Solving quantified verification conditions using satisfiability modulo theories, Annals of Mathematics and Artificial Intelligence, vol.21, issue.2, pp.101-122, 2009.
DOI : 10.1007/BF00244275
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.192.6628

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=10.1.1.150.833

Y. Gurevich, The decision problem for standard classes, The Journal of Symbolic Logic, vol.5, issue.02, pp.460-464, 1976.
DOI : 10.1007/BF01708881
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.360.1517

P. Habermehl, R. Iosif, and T. Vojnar, What Else Is Decidable about Integer Arrays?, Foundations of Software Science and Computational Structures (FOSSACS'08), pp.474-489, 2008.
DOI : 10.1007/978-3-540-78499-9_33
URL : https://hal.archives-ouvertes.fr/hal-01418914

Y. Joseph and . Halpern, Presburger arithmetic with unary predicates is ? 1 1 complete, Journal of Symbolic Logic, vol.56, issue.2, pp.637-642, 1991.

D. Harel, A. Pnueli, and J. Stavi, Propositional dynamic logic of nonregular programs, Journal of Computer and System Sciences, vol.26, issue.2, pp.222-243, 1983.
DOI : 10.1016/0022-0000(83)90014-4
URL : http://doi.org/10.1016/0022-0000(83)90014-4

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

V. A. Lifshits, Some reduction classes and undecidable theories, Studies in Constructive Mathematics and Mathematical Logic, pp.24-25, 1969.
DOI : 10.1007/978-1-4899-5630-9_6

M. Lee and M. , Computation: finite and infinite machines, 1967.

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979.
DOI : 10.1145/357073.357079
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.2828

P. Odifreddi, Classical Recursion Theory, volume 125 of Studies in Logic and the Foundations of Mathematics, 1992.

P. Moj?, ¨ Uber die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt, Sprawozdanie z I Kongresu matematyków krajów s lowia´nskichlowia´nskich, pp.92-101, 1929.

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

A. Reynolds, R. Iosif, and C. Serban, Reasoning in the Bernays?Schönfinkel? Ramsey Fragment of Separation Logic, Verification, Model Checking, and Abstract Interpretation (VMCAI'17), pp.462-482, 2017.

A. Reynolds and V. Kuncak, Induction for SMT Solvers, Verification, Model Checking, and Abstract Interpretation (VMCAI'15), pp.80-98, 2015.
DOI : 10.1007/978-3-662-46081-8_5

A. Reynolds, C. Tinelli, and L. Mendonça-de-moura, Finding conflicting instances of quantified formulas in SMT, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.195-202, 2014.
DOI : 10.1109/FMCAD.2014.6987613

H. Rogers, Theory of recursive functions and effective computability (Paperback reprint from 1967), 1987.

R. Irving and S. , Recursively Enumerable Sets and Degrees, 1987.

O. Stanislav and . Speranski, Collapsing probabilistic hierarchies. I. Algebra and Logic, pp.159-171, 2013.

O. Stanislav and . Speranski, A note on definability in fragments of arithmetic with free unary predicates, Arch. Math. Log, vol.52, pp.5-6507, 2013.

R. Stansifer, Presburger's article on integer arithmetic: Remarks and translation, 1984.