G. Alagi and C. Weidenbach, NRCL -A model building approach to the Bernays-Schönfinkel fragment, Frontiers of Combining Systems -10th International Symposium, vol.9322, pp.69-84, 2015.

P. Baumgartner, A. Fuchs, and C. Tinelli, Lemma learning in the model evolution calculus, LPAR, vol.4246, pp.572-586, 2006.

P. Baumgartner, A. Fuchs, and C. Tinelli, LIA) -model evolution with linear integer arithmetic constraints, Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, vol.5330, pp.258-273, 2008.

L. Bachmair, H. Ganzinger, and U. Waldmann, Refutational theorem proving for hierarchic first-order theories, AAECC, vol.5, issue.3/4, pp.193-212, 1994.

M. P. Bonacina and D. A. Plaisted, Semantically-guided goal-sensitive reasoning: Model representation, Journal of Automated Reasoning, vol.56, issue.2, pp.113-141, 2016.

M. Bromberger, T. Sturm, and C. Weidenbach, Linear integer arithmetic revisited, Automated Deduction -CADE-25 -25th International Conference on Automated Deduction, vol.9195, pp.623-637, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01239394

P. Baumgartner and U. Waldmann, Description Logic, Theory Combination, and All That -Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol.11560, pp.15-56, 2019.

L. Mendonça-de-moura and N. Bjørner, Engineering DPLL(T) + saturation, Automated Reasoning, 4th International Joint Conference, vol.5195, pp.475-490, 2008.

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

A. Fiori and C. Weidenbach, SCL clause learning from simple models, Automated Deduction -CADE 27 -27th International Conference on Automated Deduction, pp.233-249, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02405550

Y. Ge and L. Mendonça-de-moura, Complete instantiation for quantified formulas in satisfiabiliby modulo theories, Computer Aided Verification, 21st International Conference, pp.306-320, 2009.

H. Ganzinger and K. Korovin, New directions in instatiation-based theorem proving, Samson Abramsky, editor, 18th Annual IEEE Symposium on Logic in Computer Science, LICS'03, LICS'03, pp.55-64, 2003.

M. Horbach, M. Voigt, and C. Weidenbach, The universal fragment of presburger arithmetic with unary uninterpreted predicates is undecidable, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01592177

R. J. Bayardo and R. Schrag, Using CSP look-back techniques to solve real-world SAT instances, Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, pp.203-208, 1997.

K. Korovin, Inst-gen -A modular approach to instantiation-based automated reasoning, Programming Logics -Essays in Memory of Harald Ganzinger, vol.7797, pp.239-270, 2013.

L. Kovács and A. Voronkov, First-order theorem proving and vampire, Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification -25th International Conference, CAV 2013, vol.8044, pp.1-35, 2013.

E. Kruglov and C. Weidenbach, Superposition decides the first-order logic fragment over ground theories, Mathematics in Computer Science, vol.6, issue.4, pp.427-456, 2012.

M. L. Minsky, Computation: Finite and Infinite Machines, 1967.

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), Journal of the ACM, vol.53, pp.937-977, 2006.

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.44, issue.4, pp.401-424, 2010.

V. Prevosto, U. Waldmann, and . Spass+t, ESCoR: FLoC'06 Workshop on Empirically Successful Computerized Reasoning, vol.192, pp.18-33, 2006.

A. Reynolds, H. Barbosa, and P. Fontaine, Revisiting enumerative instantiation, Tools and Algorithms for the Construction and Analysis of Systems -24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, vol.10806, pp.112-131, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01744956

P. Rümmer, A constraint sequent calculus for first-order logic with linear integer arithmetic, LNCS, vol.5330, pp.274-289, 2008.

A. Ramos, M. Peter-van-der-tak, and . Heule, Between restarts and backjumps, Theory and Applications of Satisfiability Testing -SAT 2011 -14th International Conference, SAT 2011, vol.6695, pp.216-229, 2011.

P. M. João, K. A. Silva, and . Sakallah, Grasp -a new search algorithm for satisfiability, International Conference on Computer Aided Design, ICCAD, pp.220-227, 1996.

A. Teucke and C. Weidenbach, First-order logic theorem proving and model building via approximation and instantiation, Frontiers of Combining Systems, 10th International Symposium, vol.9322, pp.85-100, 2015.

M. Voigt, The Bernays-Schönfinkel-Ramsey fragment with bounded difference constraints over the reals is decidable, Frontiers of Combining Systems -11th International Symposium, vol.10483, pp.244-261, 2017.

C. Weidenbach, Automated reasoning building blocks, Correct System Design -Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, vol.9360, pp.172-188, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01239428