F. Ajili and É. Contejean, Complete solving of linear Diophantine equations and inequations without adding variables, Proc. First International Conference on Principles and Practice of Constraint Programming, pp.1-17, 1995.
DOI : 10.1007/3-540-60299-2_1

F. Ajili and É. Contejean, Avoiding slack variables in the solving of linear diophantine equations and inequations, Theoretical Computer Science, vol.173, issue.1, pp.183-208, 1997.
DOI : 10.1016/S0304-3975(96)00195-8

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

M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, Interactive Theorem Proving This work was supported in part by the french ANR DECERT initiative, 2010.
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.archives-ouvertes.fr/inria-00502496

M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., Verifying SAT and SMT in Coq for a fully automated decision procedure, PSATTT'11 : International Workshop on Proof-Search in Axiomatic Theories and Type Theories, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00614041

T. Arts and J. Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000.
DOI : 10.1016/S0304-3975(99)00207-8

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

V. Benzaken, É. Contejean, and S. Dumbrava, A Coq Formalization of the Relational Data Model, European Symposium on Programming, pp.189-208, 2014.
DOI : 10.1007/978-3-642-54833-8_11
URL : https://hal.archives-ouvertes.fr/hal-00924156

G. Birkhoff, On the structure of abstract algebras, Proc. Cambridge Phil. Society, p.31, 1935.

F. Bobot, S. Conchon, É. Contejean, M. Iguernelala, S. Lescuyer et al., The Alt-Ergo automated theorem prover, 2008.

F. Bobot, S. Conchon, É. Contejean, M. Iguernelala, A. Mahboubi et al., A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic, IJCAR 2012 : Proceedings of the 6th International Joint Conference on Automated Reasoning, pp.67-81, 2012.
DOI : 10.1007/978-3-642-31365-3_8
URL : https://hal.archives-ouvertes.fr/hal-00687640

F. Bobot, S. Conchon, É. 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

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/978-3-540-78800-3_24
URL : https://hal.archives-ouvertes.fr/inria-00591414

A. Boudet, É. Contejean, and H. Devie, A new AC unification algorithm with an algorithm for solving systems of diophantine equations, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.289-299, 1990.
DOI : 10.1109/LICS.1990.113755

N. Bourbaki, Eléments de mathématique ; théorie des ensembles, chapter IV, 1970.

S. Robert, J. Boyer, and . Strother-moore, Proving Theorems about LISP Functions, Journal of the ACM, vol.22, issue.1, pp.129-144, 1975.

A. Chlipala, J. G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky, Effective interactive proofs for higher-order imperative programs, pp.79-90, 2009.

S. Conchon and É. Contejean, The Alt-Ergo automatic theorem prover, APP deposit under the number, 2008.

É. Sylvain-conchon, M. Contejean, and . Iguernelala, Ground Associative and Commutative Completion Modulo Shostak Theories, LPAR, 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair Proceedings, 2010.

É. Sylvain-conchon, M. Contejean, and . Iguernelala, Canonized Rewriting and Ground AC Completion Modulo Shostak Theories, Parosh A. Abdulla Évelyne Contejean Mémoire d'Habilitation ? Université Paris-Sud (XI)

M. Rustan and . Leino, Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol.6605, pp.45-59, 2011.

É. Sylvain-conchon, M. Contejean, and . Iguernelala, Canonized rewriting and ground AC completion modulo Shostak theories : Design and implementation Selected Papers of the Conference Tools and Algorithms for the Construction and Analysis of Systems, Logical Methods in Computer Science, vol.8, issue.3, pp.1-29, 2011.

É. Sylvain-conchon, J. Contejean, and . Kanig, CC(X) : Efficiently combining equality and solvable theories without canonizers, SMT 2007 : 5th International Workshop on Satisfiability Modulo, 2007.

É. Sylvain-conchon, J. Contejean, S. Kanig, and . Lescuyer, Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant, Proceedings of the second workshop on Automated formal methods, pp.55-59, 2007.

É. Sylvain-conchon, J. Contejean, S. Kanig, and . Lescuyer, CC(X): Semantic Combination of Congruence Closure with Solvable Theories, Post-proceedings of the 5th International Workshop on Satisfiability Modulo Theories, pp.51-69, 2007.
DOI : 10.1016/j.entcs.2008.04.080

É. Contejean, Solving linear diophantine constraints incrementally, Proceedings of the 10th International Conference on Logic Programming, Logic Programming, pp.532-549, 1993.

É. Contejean, A Certified AC Matching Algorithm, van Oostrom, pp.70-84
DOI : 10.1007/978-3-540-25979-4_5

É. Contejean, Modeling Permutations in Coq for Coccinelle, Rewriting, Computation and Proof, pp.259-269, 2007.
DOI : 10.1007/978-3-540-73147-4_13

É. Contejean, Coccinelle, a Coq library for rewriting, Types, 2008.

É. Contejean and P. Corbineau, Reflecting Proofs in First-Order Logic with Equality, 20th International Conference on Automated Deduction (CADE-20), pp.7-22, 2005.
DOI : 10.1007/11532231_2
URL : https://hal.archives-ouvertes.fr/hal-00946061

É. Contejean, P. Courtieu, J. Forest, A. Paskevich, O. Pons et al., A3PAT, an approach for certified automated termination proofs, Proceedings of the ACM SIGPLAN 2010 workshop on Partial evaluation and program manipulation, PEPM '10, pp.63-72, 2010.
DOI : 10.1145/1706356.1706370
URL : https://hal.archives-ouvertes.fr/inria-00535655

É. Contejean, P. Courtieu, J. Forest, O. Pons, and X. Urbain, Certification of Automated Termination Proofs, 6th International Symposium on Frontiers of Combining Systems (FroCos 07, pp.148-162, 2007.
DOI : 10.1007/978-3-540-74621-8_10
URL : https://hal.archives-ouvertes.fr/hal-01125312

É. Contejean, P. Courtieu, J. Forest, O. Pons, and X. Urbain, Automated Certified Proofs with CiME3, 22nd International Conference on Rewriting Techniques and Applications (RTA 11), volume 10 of Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, pp.21-30, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00777669

É. Contejean and H. Devie, An Efficient Incremental Algorithm for Solving Systems of Linear Diophantine Equations, Information and Computation, vol.113, issue.1, pp.143-172, 1994.
DOI : 10.1006/inco.1994.1067

É. Contejean and C. Marché, CiME: Completion modulo E, 7th International Conference on Rewriting Techniques and Applications, pp.416-419, 1996.
DOI : 10.1007/3-540-61464-8_70

É. Contejean, C. Marché, B. Monate, and X. Urbain, Proving termination of rewriting with CiME, pp.71-73

É. Contejean, C. Marché, A. P. Tomás, and X. Urbain, Mechanically Proving Termination Using Polynomial Interpretations, Journal of Automated Reasoning, vol.12, issue.1, pp.325-363, 2005.
DOI : 10.1007/s10817-005-9022-x
URL : https://hal.archives-ouvertes.fr/inria-00001167

É. Contejean and X. Urbain, The A3PAT approach, Workshop on Certified Termination WScT08, 2008.

P. Corbineau, Démonstration Automatique en Théorie des Types, Thèse de doctorat, 2005.

J. Couchot and S. Lescuyer, Handling Polymorphism in Automated Deduction, 21th International Conference on Automated Deduction (CADE- 21), pp.263-278, 2007.
DOI : 10.1007/978-3-540-73595-3_18

M. Dauchet, Simulation of Turing machines by a left-linear rewrite rule, Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, 1989.
DOI : 10.1007/3-540-51081-8_103

M. Davis, The early history of automated deduction, Handbook of Automated Reasoning, pp.3-15, 2001.

M. Davis, G. Logemann, and D. W. 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, M. , and N. Bjørner, Z3, an efficient SMT solver

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3

N. Dershowitz, Termination dependencies, Rubio [100], pp.27-30

N. Dershowitz and J. Jouannaud, Notations for rewriting, EATCS Bulletin, vol.43, pp.162-172, 1990.

N. Dershowitz and Z. Manna, Proving termination with multiset orderings, Communications of the ACM, vol.22, issue.8, pp.465-476, 1979.
DOI : 10.1145/359138.359142

J. Peter, R. Downey, R. E. Sethi, and . Tarjan, Variations on the common subexpressions problem, Journal of the ACM, vol.27, issue.4, pp.771-785, 1980.

C. Dross, J. Sylvain-conchon, A. Kanig, and . Paskevich, Reasoning with triggers, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00703207

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

O. Fissore, I. Gnaedig, and H. Kirchner, CARIBOO : A multistrategy termination proof tool based on induction, Proceedings of the 6th International Workshop on Termination 2003, pp.77-79, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099467

J. Giesl, P. Schneider-kamp, and R. Thiemann, AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework, Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR '06), pp.281-286, 2006.
DOI : 10.1007/11814771_24

J. Giesl, R. Thiemann, P. Schneider-kamp, and S. Falke, Mechanizing and Improving Dependency Pairs, Journal of Automated Reasoning, vol.34, issue.2, pp.155-203, 2006.
DOI : 10.1007/s10817-006-9057-7

C. Paul and . Gilmore, A program for the production from axioms, of proofs for theorems derivable within the first order predicate calculus, IFIP Congress, pp.265-272, 1959.

C. Gonzalia, Towards a??Formalisation of Relational Database Theory in Constructive Type Theory, RelMiCS, pp.137-148, 2003.
DOI : 10.1007/978-3-540-24771-5_12

C. Gonzalia, Relations in Dependent Type Theory, 2006.

G. Grätzer, Universal Algebra, 1979.
DOI : 10.1007/978-0-387-77487-9

J. Herbrand, Recherches sur la théorie de la démonstration, Thèse d'Etat Also in : Ecrits logiques de Jacques, 1930.

N. Hirokawa and A. Middeldorp, Tyrolean Termination Tool, pp.474-511, 2007.
DOI : 10.1007/978-3-540-32033-3_14

G. Huet, A complete proof of correctness of the Knuth-Bendix completion algorithm, Journal of Computer and System Sciences, vol.23, issue.1, pp.11-21, 1981.
DOI : 10.1016/0022-0000(81)90002-7
URL : https://hal.archives-ouvertes.fr/inria-00076536

G. Huet and D. S. Lankford, On the uniform halting problem for term rewriting systems, Research Report, vol.283, 1978.

J. Hullot, Associative commutative pattern matching, Proc. 6th IJCAI, pp.406-412, 1979.

M. Iguernelala, Strengthening the Heart of an SMT-Solver : Design and Implementation of Efficient Decision Procedures, Thèse de doctorat, 2013.
URL : https://hal.archives-ouvertes.fr/tel-00842555

J. Jouannaud and A. Rubio, The higher-order recursive path ordering, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), 1999.
DOI : 10.1109/LICS.1999.782635

S. Kamin and J. Lévy, Two generalizations of the recursive path ordering Available as a report of the department of computer science, 1980.

C. Kirchner, Méthodes et outils de conception systématique d'algorithmes d'unification dans les théories equationnelles, Thèse d'Etat, 1985.

C. Kirchner and F. Klay, Syntactic theories and unification, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, 1990.
DOI : 10.1109/LICS.1990.113753

E. Donald, P. B. Knuth, and . Bendix, Simple word problems in universal algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970.

A. Koprowski, Certified Higher-Order Recursive Path Ordering, 17th International Conference on Rewriting Techniques and Applications (RTA'06), pp.227-241, 2006.
DOI : 10.1007/11805618_17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.3017

S. Krsti´ckrsti´c and S. Conchon, Canonization for disjoint unions of theories, Information and Computation, vol.199, issue.1-2, pp.87-106, 2005.
DOI : 10.1016/j.ic.2004.11.001

D. S. Lankford, On proving term rewriting systems are Noetherian, 1979.

J. Largeault, Logique Mathématique, textes. Collection U, 1972.

P. Lescanne, term rewriting system generator, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '83, 1983.
DOI : 10.1145/567067.567078

P. Lescanne, Implementation of completion by transition rules + control: ORME, Proceedings of the Second International Conference on Algebraic and Logic Programming, 1990.
DOI : 10.1007/3-540-53162-9_44

S. Lescuyer, Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq, Thèse de doctorat, 2011.

S. Lucas, mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting, pp.200-209
DOI : 10.1007/978-3-540-25979-4_14

G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky, Toward a verified relational database management system, ACM International Conference on Principles of Programming Languages (POPL), 2010.

Z. Manna and S. Ness, On the termination of markov algorithms, Proc. third Hawaii International Conference on Systems Sciences, pp.789-792, 1970.

Y. V. Matiyasevich, Enumerable sets are diophantine, Soviet Mathematics (Dokladi ), vol.11, issue.2, pp.354-357, 1970.

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

A. Newell, J. C. Shaw, and H. A. Simon, Report on a general problemsolving program, IFIP Congress, pp.256-264, 1959.

T. Nipkow, Proof transformations for equational theories, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, 1990.
DOI : 10.1109/LICS.1990.113754

E. Ohlebusch, C. Claves, and C. Marché, TALP: A Tool for the Termination Analysis of Logic Programs, 11th International Conference on Rewriting Techniques and Applications, pp.270-273, 2000.
DOI : 10.1007/10721975_20

A. David and . Plaisted, A recursively defined ordering for proving termination of term rewriting systems, 1978.

D. Prawitz, H. Prawitz, and N. Voghera, A Mechanical Proof Procedure and its Realization in an Electronic Computer, Journal of the ACM, vol.7, issue.2, pp.102-128, 1960.
DOI : 10.1145/321021.321023

R. Ramakrishnan and J. Gehrke, Database management systems (3

R. Iturriga, Contributions to Mechanical Mathematics, 1967.

J. A. Robinson, Automatic Deduction with Hyper-Resolution, International Journal of Computer Mathematics, vol.1, pp.227-234, 1965.
DOI : 10.1007/978-3-642-81952-0_27

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. S. Scott, A type-theoretical alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science, vol.121, issue.1-2, pp.411-440, 1993.
DOI : 10.1016/0304-3975(93)90095-B

G. Sutcliffe, C. Suttner, and T. Yemenis, The TPTP problem library, Proc. 12th Conference on Automated Deduction CADE, pp.252-266, 1994.
DOI : 10.1007/3-540-58156-1_18

A. M. Turing, On computable numbers, with an application to the Entscheidungsproblem, Proc. London Math. Soc, vol.42, issue.2, pp.230-265, 1936.

A. M. Turing, On computable numbers, with an application to the Entscheidungsproblem, Proc. London Math. Soc, vol.43, pp.544-546, 1937.

J. D. Ullman, Principles of Database Systems, 1982.

J. Van-leeuwen, Handbook of Theoretical Computer Science : Volume B : Formal Models and Semantics, 1990.

L. Vigneron, Déduction automatique avec contraintes symboliques dans les théories equationnelles, Thèse de doctorat, 1994.

A. North and W. , A treatise on universal algebra, with applications, 1898.

A. North, W. , B. A. , and W. Russell, Principia mathematica, 1927.

. Implanter and C. Cime, 36 3.2.1 Comment implanter une algèbre universelle ?, p.36