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, Hyper tableau -the next generation, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX '98, vol.1397, pp.60-76, 1998.

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

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

C. G. Fermüller and R. Pichler, Model representation over finite and infinite signatures, J. Log. Comput, vol.17, issue.3, pp.453-477, 2007.

A. Fiori and C. Weidenbach, Scl clause learning from simple models, 27th International Conference on Automated Deduction, vol.11716, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02405550

T. Hillenbrand and C. Weidenbach, Superposition for bounded domains, McCune Festschrift, vol.7788, pp.68-100, 2013.

B. Kaufmann, N. Leone, S. Perri, and T. Schaub, Grounding and solving in answer set programming, AI Magazine, vol.37, issue.3, pp.25-32, 2016.

K. Korovin, Inst-gen -A modular approach to instantiation-based automated reasoning, Lecture Notes in Computer Science, vol.7797, pp.239-270, 2013.

K. Korovin, Non-cyclic sorts for first-order satisfiability, Frontiers of Combining Systems -9th International Symposium, vol.8152, pp.214-228, 2013.

H. R. Lewis, Complexity results for classes of quantificational formulas, Journal of Compututer and System Sciences, vol.21, issue.3, pp.317-353, 1980.

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.

J. A. Pérez and A. Voronkov, Proof systems for effectively propositional logic, Automated Reasoning, 4th International Joint Conference, pp.426-440, 2008.

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

D. A. Plaisted, Complete problems in the first-order predicate calculus, Journal of Computer and System Sciences, vol.29, pp.8-35, 1984.

G. Sutcliffe, The CADE ATP System Competition -CASC, AI Magazine, vol.37, issue.2, pp.99-101, 2016.

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.