. [. Bibliography, . Avenhaus, . Th, B. Hillenbrand, and . Löchner, On using ground joinable equations in equational theorem proving, Journal of Symbolic Computation, vol.36, issue.12, pp.217-233, 2003.

S. Abiteboul, R. Hull, and V. Vianu, Foundations of Databases, 1995.

E. Ernst-althaus, C. Kruglov, and . Weidenbach, Superposition Modulo Linear Arithmetic SUP(LA), Frontiers of Combining Systems, pp.84-99, 2009.

A. Asperti and E. Tassi, Smart Matching, Intelligent Computer Mathematics, pp.263-277, 2010.
DOI : 10.1007/978-3-642-14128-7_23

[. Blanchette, L. Bulwahn, and T. Nipkow, Automatic Proof and Disproof in Isabelle/HOL, Frontiers of Combining Systems, pp.12-27
DOI : 10.1007/BFb0028402

J. Christian-blanchette, S. Böhme, A. Popescu, and N. Smallbone, Encoding Monomorphic and Polymorphic Types, Tools and Algorithms for the Construction and Analysis of Systems, pp.493-507
DOI : 10.1007/978-3-642-36742-7_34

G. Burel and S. Cruanes, Detection of First Order Axiomatic Theories, Frontiers of Combining Systems, pp.229-244, 2013.
DOI : 10.1007/978-3-642-40885-4_16
URL : https://hal.archives-ouvertes.fr/hal-00919759

S. Bobot, E. Conchon, and . Contejean, Mohamed Iguernelala, Stéphane Lescuyer, and Alain Mebsout. The Alt-Ergo automated theorem prover, 2008.

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

L. Bachmair and H. Ganzinger, Rewrite techniques for transitive relations, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.384-393, 1994.
DOI : 10.1109/LICS.1994.316051

L. Bachmair and H. Ganzinger, Associative-commutative superposition, Conditional and Typed Rewriting Systems, 1995.
DOI : 10.1007/3-540-60381-6_1

L. Bachmair, H. Ganzinger, and U. Waldmann, Refutational theorem proving for hierarchic first-order theories Applicable Algebra in Engineering, Communication and Computing, vol.5, pp.3-4193, 1994.

A. Biere, Resolve and Expand, Proc. 7th Intl. Conf. on Theory and Applications of Satisfiability Testing, 2004.
DOI : 10.1007/11527695_5

A. Bouhoula, E. Kounalis, and M. Rusinowitch, SPIKE, an automatic theorem prover, Logic Programming and Automated Reasoning, 1992.
DOI : 10.1007/BFb0013087

S. Robert, J. Boyer, and . Strother-moore, A Computational Logic Handbook: Formerly Notes and Reports in Computer Science and Applied Mathematics, 2014.

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

F. Baader and W. Snyder, Unification theory, Robinson and Voronkov [RV01c], pp.445-532

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.
DOI : 10.1016/0004-3702(93)90079-Q

[. Benzmüller, F. Theiss, L. Paulson, and A. Fietzke, LEO-II a cooperative automatic theorem prover for higher-order logic, Automated Reasoning, 4th International Joint Conference Proceedings, pp.162-170, 2008.

[. Baumgartner and U. Waldmann, Hierarchic Superposition with Weak Abstraction, Automated Deduction?CADE-24, 2013.
DOI : 10.1007/978-3-642-38574-2_3
URL : https://hal.archives-ouvertes.fr/hal-00931919

É. Bézout, Théorie générale des équations algébriques

A. Church, An Unsolvable Problem of Elementary Number Theory, American Journal of Mathematics, vol.58, issue.2, pp.345-363, 1936.
DOI : 10.2307/2371045

M. Cjrs12-]-koen-claessen, D. Johansson, N. Rosén, and . Smallbone, Hipspec: Automating inductive proofs of program properties, ATx/WInG@ IJCAR. Citeseer, 2012.

E. Contejean, C. Marché, and L. Rabehasaina, Rewrite systems for natural, integral, and rational arithmetic, Rewriting Techniques and Applications, pp.98-112, 1997.
DOI : 10.1007/3-540-62950-5_64

A. Stephen and . Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing, pp.151-158, 1971.

C. David and . Cooper, Theorem proving in arithmetic without multiplication, Machine Intelligence, 1972.

[. Bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indagationes Mathematicae (Proceedings), volume, pp.381-392, 1972.

[. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01199506

[. Dershowitz and Z. Manna, Proving termination with multiset orderings, dMB08] Leonardo de Moura and Nikolaj Bjørner. Engineering DPLL(T) + saturation Proc. 4TH IJCAR, pp.465-476, 1979.
DOI : 10.1145/359138.359142

G. Dowek, Polarized Resolution Modulo, CristianS. Calude and Vladimiro Sassone Theoretical Computer Science IFIP Advances in Information and Communication Technology, pp.182-196, 2010.
DOI : 10.1007/978-3-642-15240-5_14
URL : https://hal.archives-ouvertes.fr/hal-01054460

[. Filliâtre and S. Conchon, Type-safe modular hash-consing, Proceedings of the 2006 workshop on ML , ML '06
DOI : 10.1145/1159876.1159880

A. Fietzke and C. Weidenbach, Labelled splitting, Annals of Mathematics and Artificial Intelligence, vol.21, issue.2, pp.3-34, 2009.
DOI : 10.1007/s10472-009-9150-9
URL : http://dx.doi.org/10.1007/s10472-009-9150-9

[. Ganzinger, R. Nieuwenhuis, and P. Nivela, The Saturate system, 1998.

H. Ganzinger and J. Stuber, Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation, Lecture Notes in Computer Science, vol.2741, pp.335-349, 2003.
DOI : 10.1007/978-3-540-45085-6_31
URL : https://hal.archives-ouvertes.fr/inria-00099710

[. Hillenbrand, A. Jaeger, and B. Löchner, System Description: Waldmeister ??? Improvements in Performance and Ease of Use, Automated Deduction ? CADE-16, pp.232-236, 1999.
DOI : 10.1007/3-540-48660-7_20

G. Huet, G. Kahn, and C. Paulin-mohring, The coq proof assistant. A Tutorial. Version, 1997.
URL : https://hal.archives-ouvertes.fr/inria-00070034

L. [. Johansson, A. Dixon, and . Bundy, Conjecture Synthesis for Inductive Theories, Journal of Automated Reasoning, 2010.
DOI : 10.1007/s10817-010-9193-y

R. [. Kaufmann and . Boyer, The Boyer-Moore Theorem Prover and Its Interactive Enhancement, Computers and Mathematics with Applications, 1995.

[. Büning, M. Karpinski, and A. Flogel, Resolution for Quantified Boolean Formulas, Information and Computation, vol.117, issue.1, pp.12-18, 1995.
DOI : 10.1006/inco.1995.1025

[. Korovin, iProver ??? An Instantiation-Based Theorem Prover for First-Order Logic (System Description), Proceedings of the 4th international joint conference on Automated Reasoning, IJCAR '08, pp.292-298, 2008.
DOI : 10.1007/978-3-540-71070-7_24

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

D. Kroening and O. Strichman, Decision Procedures, An Algorithmic Point of View, 2008.

K. Korovin and C. Sticksel, Labelled Unit Superposition Calculi for Instantiation-Based Reasoning, Logic for Programming, pp.459-473, 2010.
DOI : 10.1007/978-3-642-16242-8_33

K. Korovin and A. Voronkov, Integrating Linear Arithmetic into Superposition Calculus, Computer Science Logic, pp.223-237, 2007.
DOI : 10.1007/978-3-540-74915-8_19

T. Lev-ami and C. Weidenbach, Labelled Clauses, Automated Deduction ? CADE-21, pp.311-327, 2007.
DOI : 10.1007/978-3-540-73595-3_21

F. Lonsing and A. Biere, DepQBF: A Dependency-Aware QBF Solver, Journal on Satisfiability, Boolean Modeling and Computation, 2010.

W. Mccune, OTTER 3.0 Reference Manual and Guide, 1995.
DOI : 10.2172/10129052

W. Mccune, Solution of the Robbins Problem, Journal of Automated Reasoning, vol.19, issue.3, pp.263-276, 1997.
DOI : 10.1023/A:1005843212881

W. Mccune, Prover9 and Mace4, 2005.

[. 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

G. Nelson and D. C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM, vol.27, issue.2, pp.356-364, 1980.
DOI : 10.1145/322186.322198

[. Nipkow, C. Lawrence, M. Paulson, and . Wenzel, Isabelle/HOL: a proof assistant for higher-order logic, 2002.
DOI : 10.1007/3-540-45949-9

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving, Robinson and Voronkov [RV01c]
DOI : 10.1016/B978-044450813-3/50009-6

[. Nieuwenhuis, J. Rivero, and M. Vallejo, Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses, Lecture Notes in Computer Science, vol.1249, pp.49-52, 1997.
DOI : 10.1007/3-540-63104-6_5

A. Nonnengart and C. Weidenbach, Computing Small Clause Normal Forms, Robinson and Voronkov [RV01c], pp.335-367
DOI : 10.1016/B978-044450813-3/50008-4

[. Pelletier, Seventy-five problems for testing automatic theorem provers, Journal of Automated Reasoning, vol.26, issue.8, pp.191-216, 1986.
DOI : 10.1007/BF02432151

A. Reynolds and V. Kuncak, Induction for SMT Solvers, Verification, Model Checking, and Abstract Interpretation (VMCAI), 2015.
DOI : 10.1007/978-3-662-46081-8_5

]. J. [-rob65 and . Robinson, A Machine-Oriented Logic Based on the Resolution Principle, J. ACM, vol.12, issue.1, pp.23-41, 1965.

]. J. [-rob71 and . Robinson, Computational logic: The unification computation, Machine intelligence, vol.6, pp.63-7210, 1971.

H. Rueß and N. Shankar, Deconstructing Shostak. To be presented at, 2001.

R. [. Ramakrishnan, A. Sekar, and . Voronkov, Term indexing, Robinson and Voronkov [RV01c], pp.1853-1964

P. Rümmer, A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic, Logic for Programming, pp.274-289, 2008.
DOI : 10.1007/978-3-540-89439-1_20

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.

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

S. Schulz, Simple and Efficient Clause Subsumption with Feature Vector Indexing, Proc. of the IJCAR-2004 Workshop on Empirically Successful First-Order Theorem Proving, 2004.
DOI : 10.1007/BF00881918

S. Schulz, Fingerprint Indexing for Paramodulation and Rewriting, Automated Reasoning, pp.477-483, 2012.
DOI : 10.1007/978-3-642-31365-3_37
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.297.36

G. Smolka, Logic Programming over Polymorphically Order-Sorted Types, 1989.

C. [. Sutcliffe and . Suttner, The State of CASC, AI Communications, vol.19, issue.1, pp.35-48, 2006.

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

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

]. G. Tse83 and . Tseitin, On the Complexity of Derivation in Propositional Calculus, Automation of Reasoning, Symbolic Computation, pp.466-483, 1983.

A. Voronkov, AVATAR: The Architecture for First-Order Theorem Provers, Computer Aided Verification -26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 Proceedings, pp.696-710, 2014.
DOI : 10.1007/978-3-319-08867-9_46

U. Waldmann, Extending reduction orderings to ACU-compatible reduction orderings, Information Processing Letters, vol.67, issue.1, pp.43-49, 1998.
DOI : 10.1016/S0020-0190(98)00084-2

U. Waldmann, Superposition and Chaining for Totally Ordered Divisible Abelian Groups, IJCAR, Lecture Notes in Computer Science, 2001.
DOI : 10.1007/3-540-45744-5_17

C. Weidenbach, R. Schmidt, and T. Hillenbrand, System Description: Spass Version 3.0, Lecture Notes in Computer Science, vol.4603, pp.514-520, 2007.
DOI : 10.1007/978-3-540-73595-3_38

[. Zhang, D. Kapur, M. S. Krishnamoorthy, and .. , A mechanizable induction principle for equational specifications, 9th International Conference on Automated Deduction List of Figures 2.1 Inference rules of Superposition, pp.162-181, 1988.
DOI : 10.1007/BFb0012831

.. Some-simplification-rules, 23 2.3 Simplification Rules using Subsumption, p.25

_. Declaration-of-scoped, .. , and F. , 28 3.2 View and Constructor for Type, p.31