N. Amin, S. Grütter, M. Odersky, T. Rompf, and S. Stucki, The Essence of Dependent Object Types, List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pp.249-272, 2016.
DOI : 10.1145/1993498.1993570

M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Certified Programs and Proofs: First International Conference Proceedings, pp.135-150, 2011.
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130

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

L. Bachmair and H. Ganzinger, On restrictions of ordered paramodulation with simplification, 10th International Conference on Automated Deduction, pp.427-441, 1990.
DOI : 10.1007/3-540-52885-7_105

L. Bachmair and H. Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.217-247, 1994.
DOI : 10.1093/logcom/4.3.217

L. Bachmair and H. Ganzinger, Equational reasoning in saturation-based theorem proving Automated Deduction: A Basis for Applications, volume I, pp.353-397, 1998.

C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB Standard: Version 2.5, 2015.
DOI : 10.1007/978-3-642-19583-9_2

C. Benzmüller, L. C. Paulson, F. Theiss, and A. Fietzke, LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description), Automated Reasoning: 4th International Joint Conference Proceedings, pp.162-170, 2008.
DOI : 10.1007/978-3-540-71070-7_14

J. Blanchette, A. Popescu, D. Wand, and C. Weidenbach, More SPASS with Isabelle, Interactive Theorem Proving, pp.345-360, 2012.
DOI : 10.1007/978-3-642-32347-8_24
URL : https://hal.archives-ouvertes.fr/hal-00760392

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, Journal of Automated Reasoning, vol.13, issue.5, pp.109-128, 2013.
DOI : 10.1016/B978-044450813-3/50029-1

J. C. Blanchette, S. Böhme, A. Popescu, and N. Smallbone, Encoding monomorphic and polymorphic types, Logical Methods in Computer Science, vol.12, issue.4, p.2016
DOI : 10.1007/978-3-642-36742-7_34

J. C. Blanchette and A. Paskevich, TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism, Automated Deduction ? CADE-24: 24th International Conference on Automated Deduction, Lake Placid Proceedings, pp.414-420, 2013.
DOI : 10.1007/978-3-642-38574-2_29
URL : https://hal.archives-ouvertes.fr/hal-00825086

F. Bobot, S. Conchon, E. Contejean, and S. Lescuyer, Implementing polymorphism in SMT solvers, Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, SMT '08/BPR '08, pp.1-5, 2008.
DOI : 10.1145/1512464.1512466
URL : http://www.lri.fr/~conchon/publis/conchon-smt08.pdf

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, Workshop on Intermediate Verification Languages, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

F. Bobot and A. Paskevich, Expressing Polymorphic Types in a Many-Sorted Language, Frontiers of Combining Systems: 8th International Symposium Proceedings, pp.87-102, 2011.
DOI : 10.1007/3-540-45949-9
URL : https://hal.archives-ouvertes.fr/inria-00591414

H. Chamarthi, P. Dillinger, P. Manolios, and D. Vroon, The ACL2 Sedan Theorem Proving System, International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.291-295, 2011.
DOI : 10.1007/11817963_36

K. Claessen, M. Johansson, D. Rosén, and N. Smallbone, Automating Inductive Proofs Using Theory Exploration, International Conference on Automated Deduction, pp.392-406, 2013.
DOI : 10.1007/978-3-642-38574-2_27

H. Comon, Inductionless Induction, pp.913-962
DOI : 10.1016/B978-044450813-3/50016-3
URL : http://www.lsv.ens-cachan.fr/~comon/ftp.articles/hb.ps

?. Czajka and C. Kaliszyk, Goal Translation for a Hammer for Coq (Extended Abstract), First International Workshop on Hammers for Type Theories of Electronic Proceedings in Theoretical Computer Science, pp.13-20, 2016.
DOI : 10.1007/978-3-540-74591-4_28
URL : http://arxiv.org/pdf/1606.05946

L. De-moura, Lost in translation: how easy (automated reasoning) problems become hard due to bad encodings, VAMPIRE 2015, 2015.

L. De-moura and N. Bjørner, Z3: An efficient SMT solver Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software Proceedings, pp.337-340, 2008.

L. Dixon and J. Fleuriot, IsaPlanner: A Prototype Proof Planner in Isabelle, Lecture Notes in Computer Science, vol.2741, pp.279-283, 2003.
DOI : 10.1007/978-3-540-45085-6_22
URL : http://homepages.inf.ed.ac.uk/ldixon/papers/cade-03-isaplanner.pdf

L. Erkök and J. Matthews, Using Yices as an automated solver in Isabelle/HOL, Automated Formal Methods (AFM08), pp.3-13, 2008.

S. Falke and D. Kapur, Rewriting Induction + Linear Arithmetic = Decision Procedure, International Joint Conference on Automated Reasoning 2012, Proceedings, pp.241-255, 2012.
DOI : 10.1007/978-3-642-31365-3_20

M. J. Gordon and T. F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, 1993.

F. Haftmann and M. Wenzel, Constructive Type Classes in Isabelle, Types for Proofs and Programs: International Workshop, TYPES 2006, pp.160-174, 2006.
DOI : 10.1007/978-3-540-74464-1_11
URL : http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf

T. Hailperin, A theory of restricted quantification I. The Journal of Symbolic Logic, pp.19-35, 1957.

J. Harrison, HOL Light: An Overview, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, pp.60-66, 2009.
DOI : 10.1016/0304-3975(93)90095-B

L. Henkin, Completeness in the theory of types, The Journal of Symbolic Logic, vol.14, issue.02, pp.81-91, 1950.
DOI : 10.1007/BF01696781

J. Herbrand, Recherches sur la théorie de la démonstration, 1930.

C. Hritcu, A. Aguirre, C. Keller, and K. Swamy, From F to SMT, 1st International Workshop on Hammers for Type Theories, 2016.

J. Hsiang and M. Rusinowitch, Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method, Journal of the ACM, vol.38, issue.3, pp.558-586, 1991.
DOI : 10.1145/116825.116833

A. Ireland and A. Bundy, Productive use of failure in inductive proof, Journal of Automated Reasoning, vol.38, issue.149, pp.79-111, 1996.
DOI : 10.1093/mind/XXXVIII.149.1

C. Kaliszyk and J. Urban, Learning-Assisted Automated Reasoning with Flyspeck, Journal of Automated Reasoning, vol.50, issue.1???2, pp.173-213, 2014.
DOI : 10.1007/s10817-012-9269-y
URL : https://link.springer.com/content/pdf/10.1007%2Fs10817-014-9303-3.pdf

A. Kersani and N. Peltier, Combining Superposition and Induction: A Practical Realization, FroCoS 2013, Proceedings, pp.7-22, 2013.
DOI : 10.1007/978-3-642-40885-4_2
URL : https://hal.archives-ouvertes.fr/hal-00934610

D. Knuth and P. Bendix, Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

D. E. Knuth and P. B. Bendix, Simple Word Problems in Universal Algebras, Automation of Reasoning: 2: Classical Papers on Computational Logic, pp.342-376, 1967.
DOI : 10.1007/978-3-642-81955-1_23

M. Kosta and C. Weidenbach, Automated reasoning, 2012.

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

D. Lankford, Canonical inference, 1975.

K. R. Leino, Dafny: An Automatic Program Verifier for Functional Correctness, Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'10, pp.348-370, 2010.
DOI : 10.1007/978-3-540-87873-5_10
URL : http://research.microsoft.com/~leino/papers/krml203.pdf

K. R. Leino, Automating Induction with an SMT Solver, Lecture Notes in Computer Science, vol.53, issue.6, pp.315-331, 2012.
DOI : 10.1145/1375581.1375624
URL : http://research.microsoft.com/%7Eleino/papers/krml218.pdf

K. R. Leino and P. Rümmer, A polymorphic intermediate verification language: Design and logical encoding Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software. Proceedings, pp.312-327, 2010.

W. Mccune, OTTER 3.3 reference manual. CoRR, cs, 2003.

R. Milner, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978.
DOI : 10.1016/0022-0000(78)90014-4

R. Nieuwenhuis and A. Rubio, Theorem Proving with Ordering and Equality Constrained Clauses, Journal of Symbolic Computation, vol.19, issue.4, pp.321-351, 1995.
DOI : 10.1006/jsco.1995.1020
URL : https://doi.org/10.1006/jsco.1995.1020

T. Nipkow, Order-sorted polymorphism in Isabelle, Papers Presented at the Second Annual Workshop on Logical Environments, pp.164-188, 1993.

T. Nipkow and C. Prehofer, Type checking type classes, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.409-418, 1993.
DOI : 10.1145/158511.158698
URL : http://www4.informatik.tu-muenchen.de/papers/NipkowPrehofer_P2AS1993.ps.gz

T. Nipkow, M. Wenzel, and L. C. Paulson, Isabelle/HOL: A Proof Assistant for Higher-order Logic, 2002.
DOI : 10.1007/3-540-45949-9

A. Reynolds and V. Kuncak, Induction for SMT Solvers, VMCAI 2015, pp.80-98, 2015.
DOI : 10.1007/978-3-662-46081-8_5

G. Robinson and L. Wos, Paramodulation and theorem-proving in first-order theories with equality, Machine Intelligence 4, pp.133-150
DOI : 10.1142/9789812813411_0008

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

D. Rosén, M. Johansson, and N. Smallbone, Tons of inductive problems Available at https://github, pp.tip-org, 2015.

M. Schmidt-schauß, Computational aspects of an order-sorted logic with term declarations, 1988.
DOI : 10.1007/BFb0024065

S. Schulz, Simple and Efficient Clause Subsumption with Feature Vector Indexing, Automated Reasoning and Mathematics, pp.45-67, 2013.
DOI : 10.1016/B978-044450813-3/50029-1
URL : http://www4.in.tum.de/~schulz/PAPERS/Schulz2013-FVI.pdf

W. Sonnex, S. Drossopoulou, and S. Eisenbach, Zeno: An Automated Prover for Properties of Recursive Data Structures, International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.407-421, 2012.
DOI : 10.1007/978-3-642-28756-5_28

M. Stickel, The path-indexing method for indexing term, Technical Note 473. Artificial Intelligence Center, SRI International, 1989.
DOI : 10.21236/ADA460990

M. Stickel, R. Waldinger, M. Lowry, T. Pressburger, and I. Underwood, Deductive composition of astronomical software from subroutine libraries, Automated Deduction ? CADE-12: 12th International Conference on Automated Deduction Proceedings, pp.341-355, 1994.
DOI : 10.1007/3-540-58156-1_24

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, issue.2, pp.285-309, 1955.
DOI : 10.2140/pjm.1955.5.285

P. Wadler and S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '89, pp.60-76, 1989.
DOI : 10.1145/75277.75283

U. Waldmann, Semantics of order-sorted specifications, Theoretical Computer Science, vol.94, issue.1, pp.1-35, 1992.
DOI : 10.1016/0304-3975(92)90322-7
URL : https://doi.org/10.1016/0304-3975(92)90322-7

U. Waldmann, Cancellative abelian monoids and related structures in refutational theorem proving (part i), Journal of Symbolic Computation, vol.33, issue.6, 2002.
DOI : 10.1006/jsco.2002.0536
URL : https://doi.org/10.1006/jsco.2002.0536

U. Waldmann, Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II), Journal of Symbolic Computation, vol.33, issue.6, 2002.
DOI : 10.1006/jsco.2002.0537
URL : https://doi.org/10.1006/jsco.2002.0537

C. Weidenbach, Combining Superposition, Sorts and Splitting, pp.1965-2013
DOI : 10.1016/B978-044450813-3/50029-1

M. Wisniewski, A. Steen, and C. Benzmüller, LeoPARD ??? A Generic Platform for the Implementation of Higher-Order Reasoners, Intelligent Computer Mathematics: International Conference Proceedings, pp.325-330, 2015.
DOI : 10.1007/s10817-009-9143-8

. Unkown, o F a c t s I n i t i a l C o n j e c t u r e s : : 49044 ?00005 ( 1 ) {} | | minus ( minus ( s k f 2 , s k f 1 ) , s k f 3 ) = minus ( s k f 2 , minus ( s k f 1 , s k f 3 ) ) ?> . o r i g i n ( Conj, Argument, pp.7-10