R. Alur, R. Bodík, G. Juniwal, M. M. Martin, M. Raghothaman et al., Syntax-guided synthesis, 2013 Formal Methods in Computer-Aided Design, pp.1-8, 2013.
DOI : 10.1109/FMCAD.2013.6679385
URL : http://www.cis.upenn.edu/~alur/SyGuS13.pdf

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

L. Bachmair and H. Ganzinger, Resolution Theorem Proving, Handbook of automated reasoning, pp.19-99, 2001.
DOI : 10.1016/B978-044450813-3/50004-7

H. Barbosa, New techniques for instantiation and proof production in SMT solving, 2017.
URL : https://hal.archives-ouvertes.fr/tel-01591108

H. Barbosa, P. Fontaine, and A. Reynolds, Congruence Closure with Free Variables, Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp.214-230, 2017.
DOI : 10.1007/10721959_17
URL : https://hal.archives-ouvertes.fr/hal-01442691

C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB Standard: Version 2.5, 2015.

K. Claessen, A. Lillieström, and N. Smallbone, Sort It Out with Monotonicity, pp.207-221, 2011.
DOI : 10.1007/BF00243005

K. Claessen and N. Sörensson, New techniques that improve MACE-style finite model finding, Proceedings of the CADE-19 Workshop: Model Computation -Principles, 2003.

E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal et al., VCC: A Practical System for Verifying Concurrent C, pp.23-42, 2009.
DOI : 10.1007/978-3-540-74591-4_15
URL : http://research.microsoft.com/~moskal/pdf/tphol2009.pdf

M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962.
DOI : 10.1145/368273.368557

M. Davis and H. Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960.
DOI : 10.1145/321033.321034

L. De-moura and N. Bjørner, Efficient E-Matching for SMT Solvers, Proc. Conference on Automated Deduction, pp.183-198, 2007.
DOI : 10.1007/978-3-540-73595-3_13

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

H. B. Enderton, A mathematical introduction to logic, 2001.

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

Y. Ge, C. Barrett, and C. Tinelli, Solving Quantified Verification Conditions Using Satisfiability Modulo Theories, Proc. Conference on Automated Deduction (CADE), pp.167-182, 2007.
DOI : 10.1007/978-3-540-73595-3_12
URL : http://cs.nyu.edu/%7Eyeting/quantifiers.pdf

Y. Ge and L. De-moura, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification (CAV), pp.306-320, 2009.
DOI : 10.1007/978-3-540-78800-3_19

P. C. Gilmore, A proof method for quantification theory: Its justification and realization

A. Hartmanns and P. Wendler, figshare, https, 2018.

D. Jovanovic and C. Barrett, Being careful about theory combination. Formal Methods in System Design, pp.67-90, 2013.

K. Korovin, Non-cyclic Sorts for First-Order Satisfiability, Frontiers of Combining Systems (FroCoS), pp.214-228, 2013.
DOI : 10.1007/978-3-642-40885-4_15
URL : http://www.cs.man.ac.uk/~korovink/my_pub/frocos_non_cyclic_2013.pdf

L. Kovács and A. Voronkov, First-Order Theorem Proving and Vampire, Computer Aided Verification (CAV), pp.1-35, 2013.
DOI : 10.1007/978-3-642-39799-8_1

D. Prawitz, An improved proof procedure1, Theoria, vol.10, issue.no. 3, pp.102-139, 1960.
DOI : 10.1145/321021.321023

A. Reynolds, Conflicts, models and heuristics for quantifier instantiation in SMT, Vampire workshop, EPiC Series in Computing, pp.1-15, 2016.

A. Reynolds, H. Barbosa, and P. Fontaine, Revisiting enumerative instantiation -Artifact, 2018. figshare, https

A. Reynolds, C. Tinelli, and L. M. 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

A. Reynolds, C. Tinelli, A. Goel, and S. Krsti, Finite Model Finding in SMT, Computer Aided Verification (CAV), pp.640-655, 2013.
DOI : 10.1007/978-3-642-39799-8_42
URL : http://homepage.cs.uiowa.edu/%7Etinelli/papers/ReyEtAl-CAV-13.pdf

A. Reynolds, C. Tinelli, A. Goel, S. Krsti, M. Deters et al., Quantifier Instantiation Techniques for Finite Model Finding in SMT, Proc. Conference on Automated Deduction (CADE), pp.377-391, 2013.
DOI : 10.1007/978-3-642-38574-2_26

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

S. Schulz, E -a brainiac theorem prover, AI Commun, vol.15, issue.23, pp.111-126, 2002.

A. Stump, G. Sutcliffe, and C. Tinelli, StarExec: A Cross-Community Infrastructure for Logic Solving, International Joint Conference on Automated Reasoning (IJCAR), pp.367-373, 2014.
DOI : 10.1007/978-3-319-08587-6_28
URL : http://homepage.cs.uiowa.edu/%7Etinelli/papers/StuST-IJCAR-14.pdf

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/BF00263451

G. Sutcliffe, C. The, -. Atp-system-competition, and . Magazine, e;u e+u e m e;m e+m uport mport port z3 m z3 e z3 e;m z3 mport, Library # u, vol.37, issue.2, pp.99-101, 2016.