A. Voronkov, AVATAR: the architecture for first-order theorem provers, CAV 2014, pp.696-710, 2014.

L. C. Paulson and J. C. Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, 2012.

C. Kaliszyk and J. Urban, Learning-assisted automated reasoning with Flyspeck, Journal of Automated Reasoning, vol.53, issue.2, 2014.

S. Schulz, E -a brainiac theorem prover, AI Commun, vol.15, 2002.

A. Riazanov and A. Voronkov, Vampire 1.1 (system description), Proceedings of the First International Joint Conference on Automated Reasoning, IJCAR '01, pp.376-380, 2001.

C. Weidenbach, R. Schmidt, T. Hillenbrand, R. Rusev, and D. Topic, System Description: SPASS Version 3.0, Lecture Notes in Computer Science, vol.4603, pp.514-520, 2007.

L. Bachmair and H. Ganzinger, On Restrictions of Ordered Paramodulation with Simplification, 10th International Conference on Automated Deduction

. Stickel, Lecture Notes in Computer Science, vol.449, pp.427-441, 1990.

L. Kovács, S. Robillard, and A. Voronkov, Coming to terms with quantified reasoning, pp.260-270, 2017.

M. Kaufmann and J. S. Moore, ACL2: An industrial strength version of Nqthm, pp.23-34, 1996.

S. Biundo, B. Hummel, D. Hutter, and C. Walther, The Karlsruhe induction theorem proving system, International Conference on Automated Deduction, pp.672-674, 1986.

S. Stratulat, A unified view of induction reasoning for first-order logic, The Alan Turing Centenary Conference, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00763236

A. Reynolds and V. Kuncak, Induction for SMT solvers, Verification, Model Checking, and Abstract Interpretation (VMCAI), 2015.

A. Kersani and N. Peltier, Combining superposition and induction: A practical realization, Frontiers of Combining Systems, vol.8152, pp.7-22, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00934610

M. Beeson, Otter-lambda, a Theorem-prover with Untyped Lambda-unification, Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning, 2004.

D. Wand and C. Weidenbach, Automatic Induction inside Superposition, 2017.

A. Riazanov and A. Voronkov, Splitting Without Backtracking, 2001.

K. Claessen, M. Johansson, D. Rosén, and N. Smallbone, TIP: Tons of Inductive Problems, Conferences on Intelligent Computer Mathematics, pp.333-337, 2015.

A. Bundy, A. Stevens, F. Van-harmelen, A. Ireland, and A. Smaill, Rippling: A heuristic for guiding inductive proofs, Artificial Intelligence, vol.62, issue.2, pp.185-253, 1993.

R. S. Boyer and J. S. Moore, A Computational Logic Handbook: Formerly Notes and Reports in, Computer Science and Applied Mathematics, 2014.

D. Kapur and M. Subramaniam, Lemma discovery in automating induction, pp.538-552, 1996.

R. Aubin, Strategies for mechanizing structural induction, IJCAI, 1977.

G. Dowek, T. Hardin, and C. Kirchner, Theorem Proving Modulo, Journal of Automated Reasoning, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00077199

G. Burel, Embedding Deduction Modulo into a Prover, pp.155-169, 2010.

C. Barrett, P. Fontaine, and C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB), 2016.

P. Baumgartner and U. Waldmann, Hierarchic superposition with weak abstraction, Automated Deduction-CADE-24, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00931919

A. Reynolds and J. C. Blanchette, A decision procedure for (co)datatypes in SMT solvers, LNCS, vol.9195, pp.197-213, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01397082

C. Barrett, I. Shikanian, and C. Tinelli, An abstract decision procedure for satisfiability in the theory of inductive data types, J. Satisf. Boolean Model. Comput, vol.3, pp.21-46, 2007.

L. De-moura and N. Bjørner, Z3: An efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, vol.4963, pp.337-340, 2008.

M. Horbach and C. Weidenbach, Superposition for fixed domains, ACM Transactions on Computational Logic (TOCL), vol.11, issue.4, p.27, 2010.

H. Zhang, D. Kapur, and M. S. Krishnamoorthy, A mechanizable induction principle for equational specifications, 9th International Conference on Automated Deduction, vol.310, pp.162-181, 1988.

K. Claessen, M. Johansson, D. Rosén, and N. Smallbone, Hipspec: Automating inductive proofs of program properties, ATx/WInG@ IJCAR, 2012.

C. Runciman, M. Naylor, and F. Lindblad, Smallcheck and lazy smallcheck: automatic exhaustive testing for small values, Acm sigplan notices, vol.44, pp.37-48, 2008.

K. Claessen and J. Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs, Acm sigplan notices, vol.46, issue.4, pp.53-64, 2011.

F. Lindblad, Property directed generation of first-order test data, Trends in Functional Programming, pp.105-123, 2007.

S. Cruanes, Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01223502

E. Kotelnikov, L. Kovács, G. Reger, and A. Voronkov, The Vampire and the FOOL, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp.37-48, 2016.

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, Journal of Automated Reasoning, vol.43, issue.4, pp.337-362, 2009.

M. Johansson, L. Dixon, and A. Bundy, Conjecture Synthesis for Inductive Theories, Journal of Automated Reasoning, 2010.