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.

P. Baumgartner, A. Fuchs, and C. Tinelli, Lemma Learning in the Model Evolution Calculus, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-13), pp.572-586, 2006.
DOI : 10.1007/11916277_39

P. Bernays and M. Schönfinkel, Zum Entscheidungsproblem der mathematischen Logik, Mathematische Annalen, vol.86, issue.Heft 3/4, pp.342-372, 1928.
DOI : 10.1007/BF01459101

M. P. Bonacina and D. A. Plaisted, SGGS Theorem Proving: an Exposition, Workshop on Practical Aspects in Automated Reasoning (PAAR'14), EPiC 31, pp.25-38, 2014.

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

D. Bresolin, D. D. Monica, A. Montanari, and G. Sciavicco, The light side of interval temporal logic: the Bernays-Sch??nfinkel fragment of CDT, Annals of Mathematics and Artificial Intelligence, vol.1, issue.4, pp.1-311, 2014.
DOI : 10.1007/s10472-013-9337-y

W. Charatonik and P. Witkowski, On the Complexity of the Bernays? Schönfinkel Class with Datalog, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), pp.187-201, 2010.

K. Claessen and A. Lillieström, Automated Inference of Finite Unsatisfiability, Journal of Automated Reasoning, vol.19, issue.1, pp.111-132, 2011.
DOI : 10.1007/s10817-010-9216-8

B. Dreben and W. D. Goldfarb, The Decision Problem: Solvable Classes of Quantificational Formulas, 1979.

H. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1994.
DOI : 10.1007/978-1-4757-2355-7

C. G. Fermüller, A. Leitsch, U. Hustadt, and T. Tammet, Resolution Decision Procedures, Handbook of Automated Reasoning, pp.1791-1849, 2001.
DOI : 10.1016/B978-044450813-3/50027-8

P. Fontaine, Combinations of theories for decidable fragments of firstorder logic, Frontiers of Combining Systems (FroCoS'09), pp.263-278, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00430631

H. Ganzinger and K. Korovin, New directions in instantiation-based theorem proving, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.55-64, 2003.
DOI : 10.1109/LICS.2003.1210045

Y. Ge and L. M. 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-642-02658-4_25

Y. Gurevich, The Decision Problem for the Logic of Predicates and Operations. Algebra i Logika, pp.284-308, 1969.

L. Henkin, Some remarks on infinitely long formulas, Infinistic Methods, pp.167-183, 1961.

T. Hillenbrand and C. Weidenbach, Superposition for Bounded Domains, Automated Reasoning and Mathematics ? Essays in Memory of William W. McCune, pp.68-100, 2013.
DOI : 10.1007/978-3-540-71067-7_7

K. Korovin, From Resolution and DPLL to Solving Arithmetic Constraints, Frontiers of Combining Systems (FroCoS'13), pp.261-262, 2013.
DOI : 10.1007/978-3-642-40885-4_18

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

H. R. Lewis, Complexity results for classes of quantificational formulas, Journal of Computer and System Sciences, vol.21, issue.3, pp.317-353, 1980.
DOI : 10.1016/0022-0000(80)90027-6

M. Löb, Decidability of the monadic predicate calculus with unary function symbols, 22] L. Löwenheim. ¨ Uber Möglichkeiten im Relativkalkül. Mathematische Annalen, pp.563447-470, 1915.

A. Nonnengart and C. Weidenbach, Computing Small Clause Normal Forms, Handbook of Automated Reasoning, pp.335-367, 2001.
DOI : 10.1016/B978-044450813-3/50008-4

R. Piskac, L. M. 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

A. Policriti and E. Omodeo, Abstract, The Journal of Symbolic Logic, vol.75, issue.03, pp.896-918, 2012.
DOI : 10.1016/0743-1066(95)00147-6

F. P. Ramsey, On a Problem of Formal Logic, Proceedings of The London Mathematical Society, pp.2-30264, 1930.

E. Sperner, Ein Satz ???ber Untermengen einer endlichen Menge, Mathematische Zeitschrift, vol.27, issue.1, pp.544-548, 1928.
DOI : 10.1007/BF01171114

T. Sturm, M. Voigt, and C. Weidenbach, Deciding First-Order Satisfiability when Universal and Existential Variables are Separated (Extended Version) ArXiv, p.2016

C. Weidenbach, Towards an Automatic Analysis of Security Protocols in First-Order Logic, Automated Deduction (CADE-16), pp.314-328, 1999.
DOI : 10.1007/3-540-48660-7_29

T. Wies, R. Piskac, and V. Kuncak, Combining Theories with Shared Set Operations, Frontiers of Combining Systems (FroCoS'09), pp.366-382, 2009.
DOI : 10.1016/S0304-3975(01)00332-2