A. Abadi, A. Rabinovich, and M. Sagiv, Decidable fragments of many-sorted logic, Journal of Symbolic Computation, vol.45, issue.2, pp.153-172, 2010.
DOI : 10.1016/j.jsc.2009.03.003
URL : http://doi.org/10.1016/j.jsc.2009.03.003

G. Alagi and C. Weidenbach, NRCL ? A Model Building Approach to the Bernays?Schönfinkel Fragment, Frontiers of Combining Systems (FroCoS'15), pp.69-84, 2015.

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

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, Safety Analysis of Systems, 2007.

R. Aaron, Z. Bradley, and . Manna, The Calculus of Computation ? Decision Procedures with Applications to Verification, 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

K. Claessen, A. Lillieström, and N. Smallbone, Sort It Out with Monotonicity ? Translating between Many-Sorted and Unsorted First-Order Logic, Automated Deduction (CADE-23), pp.207-221, 2011.

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

Y. Joseph and . Halpern, Presburger Arithmetic with Unary Predicates is ? 1

M. Horbach, M. Voigt, and C. Weidenbach, On the Combination of the Bernays?Schönfinkel?Ramsey Fragment with Simple Linear Integer Arithmetic, ArXiv preprint, p.2017

K. Korovin, Inst-Gen ??? A Modular Approach to Instantiation-Based Automated Reasoning, Programming Logics ? Essays in Memory of Harald Ganzinger, pp.239-270, 2013.
DOI : 10.1007/s10817-009-9143-8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.225.3417

K. Korovin, Non-cyclic Sorts for First-Order Satisfiability, Frontiers of Combining Systems (FroCoS'13), pp.214-228, 2013.
DOI : 10.1007/978-3-642-40885-4_15
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.381.657

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

R. Harry and . Lewis, Complexity Results for Classes of Quantificational Formulas, Journal of Computer and System Sciences, vol.21, issue.3, pp.317-353, 1980.

R. Loos and V. Weispfenning, Applying Linear Quantifier Elimination, The Computer Journal, vol.36, issue.5, pp.450-462, 1993.
DOI : 10.1093/comjnl/36.5.450
URL : https://academic.oup.com/comjnl/article-pdf/36/5/450/1105730/360450.pdf

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006.
DOI : 10.1145/1217856.1217859

R. Piskac, L. Mendonça-de-moura, and N. Bjørner, Deciding Effectively Propositional Logic Using DPLL and Substitution Sets, Journal of Automated Reasoning, vol.53, issue.6, pp.401-424, 2010.
DOI : 10.1007/s10817-009-9161-6
URL : http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.156.8903&rep=rep1&type=pdf

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 and C. Weidenbach, Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete, ArXiv preprint, p.2015