M. Aiguier, D. Bahrami, and C. Dubois, Axioms for rewriting theory, RULE 2000: Proc. 1st International Workshop on Rule-Based Programming, 2000.
URL : https://hal.archives-ouvertes.fr/hal-01124623

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

L. Bachmair and N. Dershowitz, Completion for rewriting modulo a congruence, Theoretical Computer Science, vol.67, issue.2-3, pp.173-202, 1989.
DOI : 10.1016/0304-3975(89)90003-0

L. Bachmair and N. Dershowitz, Equational inference, canonical proofs, and proof orderings, Journal of the ACM, vol.41, issue.2, pp.236-276, 1994.
DOI : 10.1145/174652.174655

L. Bachmair, N. Dershowitz, and J. Hsiang, Orderings for equational proofs, Proc. 1st Symposium on Logic in Computer Science, pp.346-357, 1986.

L. Bachmair, N. Dershowitz, and D. Plaisted, Completion without failure, Resolution of Equations in Algebraic Structures 2: Rewriting Techniques, pp.1-30, 1989.

L. Bachmair and H. Ganzinger, Resolution Theorem Proving, Handbook of Automated Reasoning, pp.19-99, 2001.
DOI : 10.1016/B978-044450813-3/50004-7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.113.4450

B. Buchberger, Gröbner-bases: An algorithmic method in polynomial ideal theory, Multidimensional Systems Theory, chapter 6, pp.184-232, 1985.

H. Cirstea, C. Kirchner, and L. Liquori, The Rho Cube, Proc. Foundations of Software Science and Computation Structures, pp.166-180, 2001.
DOI : 10.1007/3-540-45315-6_11
URL : https://hal.archives-ouvertes.fr/inria-00107877

H. Comon and C. Kirchner, Constraint Solving on Terms, Proc. Constraints in Computational Logics. Theory and Applications, 2001.
DOI : 10.1007/3-540-45406-3_2

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, Completion and Its Applications, Resolution of Equations in Algebraic Structures, pp.31-86, 1989.
DOI : 10.1016/B978-0-12-046371-8.50008-0

N. Dershowitz, Ground canonicity. Unpublished, p.304017, 2003.

N. Dershowitz, L. Marcus, and A. Tarlecki, Existence, Uniqueness, and Construction of Rewrite Systems, SIAM Journal on Computing, vol.17, issue.4, pp.629-639, 1988.
DOI : 10.1137/0217039

N. Dershowitz and M. Okada, Proof-theoretic techniques for term rewriting theory, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.104-111, 1988.
DOI : 10.1109/LICS.1988.5108

N. Doggaz and C. Kirchner, Completion for unification, Theoretical Computer Science, vol.85, issue.2, pp.231-251, 1991.
DOI : 10.1016/0304-3975(91)90182-2
URL : http://doi.org/10.1016/0304-3975(91)90182-2

I. Gnaedig, C. Kirchner, and H. Kirchner, Equational completion in order-sorted algebras, Proc. 13th Colloquium on Trees in Algebra and Programming, pp.165-184, 1988.
DOI : 10.1016/0304-3975(90)90034-F

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.559-587, 1991.
DOI : 10.1145/116825.116833

J. Jouannaud and H. Kirchner, Completion of a Set of Rules Modulo a Set of Equations, SIAM Journal on Computing, vol.15, issue.4, pp.1155-1194, 1986.
DOI : 10.1137/0215084

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

A. Kandri-rody, D. Kapur, and F. Winkler, Knuth-Bendix procedures and Buchberger algorithm?A synthesis, Proc. 20th Intl. Symp. on Symbolic and Algebraic Computation, pp.55-67, 1989.

D. Kapur and D. R. Musser, Proof by consistency, Artificial Intelligence, vol.31, issue.2, pp.125-157, 1987.
DOI : 10.1016/0004-3702(87)90017-8

D. E. Knuth and P. B. 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. S. Lankford, Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, 1975.

Y. Métivier, About the rewriting systems produced by the Knuth-Bendix completion algorithm, Information Processing Letters, vol.16, issue.1, pp.31-34, 1983.
DOI : 10.1016/0020-0190(83)90009-1

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving, Handbook of Automated Reasoning, volume I, chapter 7, pp.371-443, 2001.
DOI : 10.1016/B978-044450813-3/50009-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.6344

G. Peterson and M. Stickel, Complete Sets of Reductions for Some Equational Theories, Journal of the ACM, vol.28, issue.2, pp.233-264, 1981.
DOI : 10.1145/322248.322251

J. Raoult, On graph rewritings, Theoretical Computer Science, vol.32, issue.1-2, pp.1-24, 1984.
DOI : 10.1016/0304-3975(84)90021-5
URL : http://doi.org/10.1016/0304-3975(84)90021-5

M. Rusinowitch, Démonstration Automatique: Techniques de Réécriture, Science Informatique. InterEditions, 1989.

M. B. Smyth, Power domains, Journal of Computer and System Sciences, vol.16, issue.1, pp.23-36, 1977.
DOI : 10.1016/0022-0000(78)90048-X

W. Snyder, Efficient ground completion, Proc. 3rd Conference on Rewriting Techniques and Applications (Chapel Hill, pp.419-433
DOI : 10.1007/3-540-51081-8_123

G. Struth, Canonical Transformations in Algebra, Universal Algebra and Logic, 1998.

M. Bezem, J. W. Klop, and R. De-vrijer, Term Rewriting Systems, 2002.

R. Virga, Higher-Order Rewriting with Dependent Types