M. Alpuente, S. Escobar, and S. Lucas, Correct and Complete (Positive) Strategy Annotations for OBJ, Proceedings of the 5th International Workshop on Rewriting Logic and its Applications (RTA), pp.70-89, 2004.
DOI : 10.1016/S1571-0661(05)82529-0

S. Anantharaman and J. Hsiang, Automated proofs of the moufang identities in alternative rings, Journal of Automated Reasoning, vol.28, issue.2, pp.79-109, 1990.
DOI : 10.1007/BF00302643

O. Andrei, M. Fernandez, H. Kirchner, G. Melançon, O. Namet et al., PORGY: Strategy-Driven Interactive Transformation of Graphs, TERMGRAPH, 6 th Int. Workshop on Computing with Terms and Graphs, pp.54-68, 2011.
DOI : 10.4204/EPTCS.48.7
URL : https://hal.archives-ouvertes.fr/inria-00563249

T. Aoto, Dealing with Non-orientable Equations in Rewriting Induction, Proceedings of the 17th International Conference on Rewriting Techniques and Applications, pp.242-256, 2006.
DOI : 10.1007/11805618_18

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

E. Astesiano, M. Bidoit, H. Kirchner, B. Krieg-brückner, P. D. Mosses et al., CASL: the Common Algebraic Specification Language, Theoretical Computer Science, vol.286, issue.2, pp.153-196, 2002.
DOI : 10.1016/S0304-3975(01)00368-1
URL : https://hal.archives-ouvertes.fr/inria-00101008

S. Autexier, D. Hutter, H. Mantel, and A. Schairer, System Description: inka 5.0 - A Logic Voyager, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pp.207-211, 1999.
DOI : 10.1007/3-540-48660-7_15

J. Avenhaus and K. Madlener, Term rewriting and equational reasoning, Formal Techniques in Artifial Intelligence, pp.1-43, 1990.

F. Baader and T. Nipkow, Term rewriting and all that, 1998.

L. Bachmair, Proof by consistency in equational theories, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, pp.228-233, 1988.
DOI : 10.1109/LICS.1988.5122

L. Bachmair, Canonical equational proofs Computer Science Logic, Progress in Theoretical Computer Science, p.15, 1991.

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, N. Dershowitz, and J. Hsiang, Orderings for equational proofs, Proceedings 1st IEEE 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, pp.1-30, 1989.

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, Resolution theorem proving. Handbook of automated reasoning, pp.19-99, 2001.

E. Balland, P. Brauner, R. Kopetz, P. Moreau, and A. Reilles, Tom: Piggybacking Rewriting on Java, Proceedings of the 18th Conference on Rewriting Techniques and Applications, pp.36-47, 2007.
DOI : 10.1007/978-3-540-73449-9_5
URL : https://hal.archives-ouvertes.fr/inria-00142045

J. A. Bergstra and J. W. Klop, Conditional rewrite rules: Confluence and termination, Journal of Computer and System Sciences, vol.32, issue.3, pp.323-362, 1986.
DOI : 10.1016/0022-0000(86)90033-4

N. Berregeb, A. Bouhoula, and M. Rusinowitch, Automated verification by induction with associative-commutative operators, Lecture Notes in Computer Science, vol.1102, pp.220-231, 1996.
DOI : 10.1007/3-540-61474-5_71

Y. Bertot and P. Casteran, Interactive Theorem Proving and Program Development, p.14, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

M. Bezem, J. W. Klop, and R. De-vrijer, Term rewriting systems, 2003.

G. Birkhoff, On the Structure of Abstract Algebras, Mathematical Proceedings of the Cambridge Philosophical Society, vol.31, issue.04, pp.433-454, 1935.
DOI : 10.1017/S0305004100013463

P. Borovanský, C. Kirchner, H. Kirchner, and P. Moreau, ELAN from a rewriting logic point of view, Theoretical Computer Science, vol.285, issue.2, pp.155-185, 2002.
DOI : 10.1016/S0304-3975(01)00358-9

P. Borovanský, C. Kirchner, H. Kirchner, and C. Ringeissen, REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS, International Journal of Foundations of Computer Science, vol.12, issue.01, pp.69-98, 1921.
DOI : 10.1142/S0129054101000412

A. Bouhoula, E. Kounalis, and M. Rusinowitch, SPIKE, an automatic theorem prover, Proceedings of the 1st International Conference on Logic Programming and Automated Reasoning, St. Petersburg (Russia), pp.460-462, 1992.
DOI : 10.1007/BFb0013087

A. Bouhoula and M. Rusinowitch, Implicit induction in conditional theories, Journal of Automated Reasoning, vol.31, issue.2, pp.189-235, 1995.
DOI : 10.1007/BF00881856
URL : https://hal.archives-ouvertes.fr/inria-00074627

T. Bourdier, H. Cirstea, D. J. Dougherty, and H. Kirchner, Extensional and Intensional Strategies, Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming of Electronic Proceedings In Theoretical Computer Science, pp.1-19, 2009.
DOI : 10.4204/EPTCS.15.1
URL : https://hal.archives-ouvertes.fr/inria-00494636

A. Bundy, The Automation of Proof by Mathematical Induction, Handbook of automated reasonning, p.14, 1999.
DOI : 10.1016/B978-044450813-3/50015-1

H. Cirstea and C. Kirchner, The rewriting calculus - part II, Logic Journal of IGPL, vol.9, issue.3, pp.427-498, 2001.
DOI : 10.1093/jigpal/9.3.377
URL : https://hal.archives-ouvertes.fr/inria-00100532

H. Cirstea, C. Kirchner, L. Liquori, and B. Wack, Rewrite Strategies in the Rewriting Calculus, Electronic Notes in Theoretical Computer Science, 2003.
DOI : 10.1016/S1571-0661(05)82613-1
URL : https://hal.archives-ouvertes.fr/inria-00099586

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., All About Maude -A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Reriting Logic, p.19, 2007.

H. Comon, Completion of rewrite systems with membership constraints, Proceedings of ICALP 92, p.12, 1992.
DOI : 10.1007/3-540-55719-9_91

H. Comon, Inductionless Induction, Handbook of Automated Reasoning, pp.914-959, 2001.
DOI : 10.1016/B978-044450813-3/50016-3

H. Comon and F. Jacquemard, Ground reducibility is exptime-complete. Information and Computation, pp.123-153, 2003.
DOI : 10.1109/lics.1997.614922
URL : https://hal.archives-ouvertes.fr/inria-00578859

H. Comon and R. Nieuwenhuis, Induction=I-Axiomatization+First-Order Consistency, Information and Computation, vol.159, issue.1-2, pp.151-186, 2000.
DOI : 10.1006/inco.2000.2875

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

M. Dauchet, Simulation of Turing machines by a left-linear rewrite rule, Rewriting Techniques and Applications (RTA'03), pp.109-120, 1989.
DOI : 10.1007/3-540-51081-8_103

D. Delahaye, A Tactic Language for the System Coq, Proceedings of Logic Programming and Automated Reasoning (LPAR), pp.85-95, 1955.
DOI : 10.1007/3-540-44404-1_7
URL : https://hal.archives-ouvertes.fr/hal-01125070

E. Deplagne, C. Kirchner, H. Kirchner, and Q. Nguyen, Proof Search and Proof Check for Equational and Inductive Theorems, Proceedings of CADE-19, p.16, 2003.
DOI : 10.1007/978-3-540-45085-6_26
URL : https://hal.archives-ouvertes.fr/inria-00099470

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, Computing with rewrite systems, Information and Control, vol.65, issue.2-3, pp.122-157, 1985.
DOI : 10.1016/S0019-9958(85)80003-6

N. Dershowitz, Termination, Rewriting Techniques and Applications, pp.180-224, 1985.
DOI : 10.1007/3-540-15976-2_9

N. Dershowitz, Termination of rewriting, Journal of Symbolic Computation, vol.3, issue.1-2, pp.69-116, 1987.
DOI : 10.1016/S0747-7171(87)80022-6

N. Dershowitz and J. Jouannaud, Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pp.244-320, 1990.

N. Dershowitz and C. Kirchner, Abstract canonical presentations, Theoretical Computer Science, vol.357, issue.1-3, pp.53-69, 2006.
DOI : 10.1016/j.tcs.2006.03.012
URL : https://hal.archives-ouvertes.fr/inria-00121760

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, M. Okada, and G. Sivakumar, Confluence of conditional rewrite systems, Proceedings 1st International Workshop on Conditional Term Rewriting Systems, pp.31-44, 1987.
DOI : 10.1007/3-540-19242-5_3

N. Dershowitz and D. A. Plaisted, Equational programming The logic and acquisition of knowledge, Machine Intelligence, pp.21-56, 1988.

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506

T. Evans, On multiplicative systems defined by generators and relations, Proceedings of the Cambridge Philosophical Society, pp.637-649, 1951.

W. Fokkink, J. Kamperman, and P. Walters, Lazy rewriting on eager machinery, ACM Transactions on Programming Languages and Systems, vol.22, issue.1, pp.45-86, 2000.
DOI : 10.1145/345099.345102

L. Fribourg, SLOG: A logic programming language intepreter based on clausal superposition and rewriting, Proceedings of the IEEE Symposium on Logic Programming, pp.172-184, 1985.

L. Fribourg, A superposition oriented theorem prover, Theoretical Computer Science, vol.35, pp.129-164, 1985.
DOI : 10.1016/0304-3975(85)90011-8

L. Fribourg, A Strong restriction of the inductive completion procedure, Proceedings 13th International Colloquium on Automata, Languages and Programming, pp.105-115, 1986.
DOI : 10.1007/3-540-16761-7_60

K. Futatsugi, J. A. Goguen, J. Jouannaud, and J. Meseguer, Principles of OBJ-2, Proceedings 12th ACM Symp. on Principles of Programming Languages, pp.52-66, 1985.

J. Giesl, P. Schneider-kamp, and R. Thiemann, AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework, Proceedings IJCAR '06, pp.281-286, 2006.
DOI : 10.1007/11814771_24

I. Gnaedig and H. Kirchner, Termination of rewriting under strategies, ACM Transactions on Computational Logic, vol.10, issue.2, pp.1-52, 2009.
DOI : 10.1145/1462179.1462182
URL : https://hal.archives-ouvertes.fr/inria-00182432

J. A. Goguen, How to prove algebraic inductive hypotheses without induction, Proceedings 5th International Conference on Automated Deduction, Les Arcs (France), pp.356-373, 1980.
DOI : 10.1007/3-540-10009-1_27

J. A. Goguen, J. Jouannaud, and J. Meseguer, Operational semantics for order-sorted algebra, Proceeding of the 12th International Colloquium on Automata, Languages and Programming, pp.221-231, 1985.
DOI : 10.1007/BFb0015747

J. A. Goguen, C. Kirchner, H. Kirchner, A. Mégrelis, J. Meseguer et al., An introduction to OBJ 3, Proceedings 1st International Workshop on Conditional Term Rewriting Systems, pp.258-263, 1920.
DOI : 10.1007/3-540-19242-5_22

J. A. Goguen and J. Meseguer, Order-sorted algebra solves the constructorselector , multiple representation and coercion problem, Proceedings 2nd IEEE Symposium on Logic in Computer Science USA), pp.18-29, 1987.

J. A. Goguen and J. Tardo, An introduction to OBJ: A language for writing and testing software specifications, Specification of Reliable Software Reprinted in Software Specification Techniques, N. Gehani and A. McGettrick, pp.170-189, 1979.

J. A. Goguen, Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theoretical Computer Science, vol.105, issue.2, pp.217-273, 1992.
DOI : 10.1016/0304-3975(92)90302-V

J. A. Goguen and J. Meseguer, EQLOG: Equality, types, and generic modules for logic programming, Functional and Logic Programming An earlier version appears in Journal of Logic Programming, pp.295-363, 1984.

B. Gramlich, Generalized sufficient conditions for modular termination of rewriting, Applicable Algebra in Engineering, Communication and Computing, vol.34, issue.1, pp.131-158, 1994.
DOI : 10.1007/BF01190827

N. Hirokawa and A. Middeldorp, Tsukuba Termination Tool, Proc. 14th Rewriting Techniques and Applications, pp.311-320, 2003.
DOI : 10.1007/3-540-44881-0_22

J. Hsiang, Refutational theorem proving using term-rewriting systems, Artificial Intelligence, vol.25, issue.3, pp.255-300, 1985.
DOI : 10.1016/0004-3702(85)90074-8

J. Hsiang, H. Kirchner, P. Lescanne, and M. Rusinowitch, The term rewriting approach to automated theorem proving, The Journal of Logic Programming, vol.14, issue.1-2, pp.71-99, 1992.
DOI : 10.1016/0743-1066(92)90047-7

J. Hsiang and M. Rusinowitch, On word problems in equational theories, Proceedings of 14th International Colloquium on Automata , Languages and Programming, pp.54-71, 1987.
DOI : 10.1007/3-540-18088-5_6
URL : https://hal.archives-ouvertes.fr/inria-00075875

G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Preliminary version in 18th Symposium on Foundations of Computer Science, pp.797-821, 1977.
DOI : 10.1145/322217.322230

G. Huet and J. Hullot, Proofs by induction in equational theories with constructors, Preliminary version in Proceedings 21st Symposium on Foundations of Computer Science, pp.239-266, 1980.
DOI : 10.1016/0022-0000(82)90006-X
URL : https://hal.archives-ouvertes.fr/inria-00076533

G. Huet and J. Lévy, Computations in orthogonal rewriting systems, I, Computational Logic, pp.395-414, 1991.

G. Huet and J. Lévy, Computations in orthogonal rewriting systems, II, Computational Logic, chapter 12, pp.415-443, 1991.

G. Huet and D. Oppen, Equations and rewrite rules: A survey Formal Language Theory: Perspectives and Open Problems, pp.349-405, 1980.

J. Hullot, Canonical forms and unification, Proceedings 5th International Conference on Automated Deduction, Les Arcs (France), pp.318-334, 1980.
DOI : 10.1007/3-540-10009-1_25

T. Isakowitz and J. Gallier, Rewriting in order-sorted equational logic, Proceedings of Logic Programming Conference, 1988.

J. Jouannaud, Confluent and coherent equational term rewriting systems application to proofs in abstract data types, Proceedings of the 8th Colloquium on Trees in Algebra and Programming, L'Aquila (Italy), pp.269-283, 1983.
DOI : 10.1007/3-540-12727-5_16

J. Jouannaud, C. Kirchner, H. Kirchner, and A. Mégrelis, OBJ: Programming with equalities, subsorts, overloading and parameterization, Journal of Logic Programming, vol.12, issue.3 7, pp.257-280, 1992.
DOI : 10.1007/3-540-50667-5_57

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 E. Kounalis, Proof by induction in equational theories without constructors, Proceedings 1st IEEE Symposium on Logic in Computer Science, pp.358-366, 1986.

J. Jouannaud and P. Lescanne, On multiset orderings, Information Processing Letters, vol.15, issue.2, pp.57-63, 1982.
DOI : 10.1016/0020-0190(82)90107-7

J. Jouannaud and B. Waldmann, Reductive conditional term rewriting systems, Proceedings of the Third IFIP Working Conference on Formal Description of Programming Concepts, p.12, 1986.

S. Kaplan, Conditional rewrite rules, Theoretical Computer Science, vol.33, issue.2-3, pp.175-193, 1984.
DOI : 10.1016/0304-3975(84)90087-2

S. Kaplan, Simplifying conditional term rewriting systems : Unification, termination and confluence, Journal of Symbolic Computation, vol.4, issue.3, pp.295-334, 1987.
DOI : 10.1016/S0747-7171(87)80010-X

D. Kapur, P. Narendran, and H. Zhang, On sufficient-completeness and related properties of term rewriting systems, Acta Informatica, vol.6, issue.5, pp.395-415, 1987.
DOI : 10.1007/BF00292110

D. Kapur and H. Zhang, An overview of Rewrite Rule Laboratory (RRL), Computers & Mathematics with Applications, vol.29, issue.2, pp.91-114, 1995.
DOI : 10.1016/0898-1221(94)00218-A

M. Kaufmann and J. S. Moore, ACL2: an industrial strength version of Nqthm, Proceedings of 11th Annual Conference on Computer Assurance. COMPASS '96, p.14, 1996.
DOI : 10.1109/CMPASS.1996.507872

C. Kirchner, F. Kirchner, and H. Kirchner, Strategic computations and deductions, Festchrift in honor of Peter Andrews, Studies in Logic and the Foundations of Mathematics, p.20, 2008.

C. Kirchner and H. Kirchner, Reveur-3: the implementation of a general completion procedure parameterized by built-in theories and strategies, Science of Computer Programming, vol.8, issue.1, pp.69-86, 1986.
DOI : 10.1016/0167-6423(87)90004-9

C. Kirchner and H. Kirchner, Constrained equational reasoning, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation , ISSAC '89, pp.382-389, 1989.
DOI : 10.1145/74540.74585

C. Kirchner, H. Kirchner, and A. Mégrelis, OBJ for OBJ, Software Engineering with OBJ: Algebraic Specification in Action, chapter 6, pp.307-330, 2000.
DOI : 10.1007/978-1-4757-6541-0_6

C. Kirchner, H. Kirchner, and J. Meseguer, Operational semantics of OBJ-3, Proceedings of 15th International Colloquium on Automata, Languages and Programming, pp.287-301, 1988.
DOI : 10.1007/3-540-19488-6_123

C. Kirchner, H. Kirchner, and F. Nahon, Narrowing Based Inductive Proof Search, Programming Logics, pp.216-238, 2013.
DOI : 10.1007/s10472-009-9154-5
URL : https://hal.archives-ouvertes.fr/hal-00692193

C. Kirchner, H. Kirchner, and M. Rusinowitch, Deduction with symbolic constraints. Revue d'Intelligence Artificielle, pp.9-52, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00077103

C. Kirchner, H. Kirchner, and M. Vittek, Designing constraint logic programming languages using computational systems, Principles and Practice of Constraint Programming, pp.131-158, 1995.

H. Kirchner, On the use of constraints in automated deduction, Constraint Programming: Basics and Trends, pp.128-146, 1995.
DOI : 10.1007/3-540-59155-9_8

J. W. Klop, Term Rewriting Systems, Handbook of Logic in Computer Science, 1990.

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

E. Kounalis, Completeness in data type specifications, Proceedings EUROCAL Conference, Linz (Austria), pp.348-362, 1985.

D. S. Lankford, A simple explanation of inductionless induction, Louisiana Tech. University, Dep. of Math, issue.14, p.15, 1981.

D. S. Lankford and A. Ballantyne, Decision procedures for simple equational theories with associative commutative axioms: complete sets of associative commutative reductions, 1977.

A. Lazrek, P. Lescanne, and J. Thiel, Tools for proving inductive equalities , relative completeness and ?-completeness. Information and Computation, pp.47-70, 1990.

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

P. Lescanne, On the recursive decomposition ordering with lexicographical status and other related orderings, Journal of Automated Reasoning, vol.3, issue.1 & 2, pp.39-49, 1990.
DOI : 10.1007/BF00302640

A. A. Letichevsky, Development of rewriting strategies, Lecture Notes in Computer Science, vol.714, issue.21, pp.378-390, 1993.
DOI : 10.1007/3-540-57186-8_92

S. Lucas, Termination of on-demand rewriting and termination of OBJ programs, Proceedings of the 3rd ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '01, pp.82-93, 2001.
DOI : 10.1145/773184.773194

S. Lucas, Termination of Rewriting with Strategy Annotations, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR'01, pp.669-684, 2001.
DOI : 10.1007/3-540-45653-8_46

N. Martí-oliet and J. Meseguer, Rewriting Logic as a Logical and Semantic Framework, Electronic Notes in Theoretical Computer Science, p.18, 2000.
DOI : 10.1007/978-94-017-0464-9_1

N. Martí-oliet, J. Meseguer, and A. Verdejo, Towards a Strategy Language for Maude, Proceedings Fifth International Workshop on Rewriting Logic and its Applications, pp.417-441, 2004.
DOI : 10.1016/j.entcs.2004.06.020

N. Martí-oliet, J. Meseguer, and A. Verdejo, A Rewriting Semantics for Maude Strategies, Electronic Notes in Theoretical Computer Science, vol.238, issue.3, pp.227-247, 2008.
DOI : 10.1016/j.entcs.2009.05.022

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

J. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, vol.96, issue.1, pp.73-155, 1992.
DOI : 10.1016/0304-3975(92)90182-F

J. Meseguer and J. A. Goguen, Initiality, induction and computability, Algebraic Methods in Semantics, 1985.

A. Middeldorp and H. Zantema, Simple termination of rewrite systems, Theoretical Computer Science, vol.175, issue.1, pp.127-158, 1997.
DOI : 10.1016/S0304-3975(96)00172-7

P. D. Mosses, CoFI: The common framework initiative for algebraic specification and development, Lecture Notes in Computer Science, vol.1214, issue.7, pp.115-137, 1997.
DOI : 10.1007/BFb0030591

D. R. Musser, On proving inductive properties of abstract data types, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '80, pp.154-162, 1980.
DOI : 10.1145/567446.567461

M. H. Newman, On Theories with a Combinatorial Definition of "Equivalence", Annals of Math, pp.223-243, 1942.
DOI : 10.2307/1968867

Q. Nguyen, Compact Normalisation Trace via Lazy Rewriting, Proceedings of the 1st International Workshop on Reduction Strategies in Rewriting and Programming, p.20, 2001.
DOI : 10.1016/S1571-0661(04)00269-5
URL : https://hal.archives-ouvertes.fr/inria-00107874

R. Nieuwenhuis and A. Rubio, Paramodulation-based theorem proving. Handbook of automated reasoning, pp.371-443, 2001.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, p.14, 2002.

E. Ohlebusch, Advanced Topics in Term Rewriting, 2002.
DOI : 10.1007/978-1-4757-3661-8

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, 11th International Conference on Automated Deduction (CADE), pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

G. Peterson and M. E. 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

D. Plaisted, Semantic confluence tests and completion methods, Information and Control, vol.65, issue.2-3, pp.182-215, 1985.
DOI : 10.1016/S0019-9958(85)80005-X
URL : http://doi.org/10.1016/s0019-9958(85)80005-x

D. Plaisted, Equational reasoning and term rewriting systems, Handbook of Logic in Artificial Intelligence and Logic Programming, pp.273-364, 1993.

U. Reddy, Term rewriting induction, Proceedings 10th International Conference on Automated Deduction, pp.162-177, 1990.
DOI : 10.1007/3-540-52885-7_86

J. Steinbach, Generating polynomial orderings, Information Processing Letters, vol.49, issue.2, pp.85-93, 1994.
DOI : 10.1016/0020-0190(94)90032-9

J. Steinbach, Simplification orderings: History of results, Fundam. Inform, vol.24, issue.12 9, pp.47-87, 1995.

M. E. Stickel, A case study of theorem proving by the Knuth-Bendix method: Discovering that x 3 = x implies ring commutativity, Proceedings 7th International Conference on Automated Deduction, pp.248-258, 1984.

J. Thiel, Stop losing sleep over incomplete data type specifications, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '84, pp.76-82, 1984.
DOI : 10.1145/800017.800518

Y. Toyama, Counterexamples to termination for the direct sum of term rewriting systems, Information Processing Letters, vol.25, issue.3, pp.141-143, 1986.
DOI : 10.1016/0020-0190(87)90122-0

E. Visser, Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5, Rewriting Techniques and Applications (RTA'01), volume 2051 of Lecture Notes in Computer Science, pp.357-361, 1921.
DOI : 10.1007/3-540-45127-7_27

H. Zantema, Termination of term rewriting: interpretation and type elimination, Journal of Symbolic Computation, vol.17, issue.1, pp.23-50, 1994.
DOI : 10.1006/jsco.1994.1003

H. Zantema, Termination of term rewriting by semantic labelling, Fundamenta Informaticae, vol.24, issue.1 9, pp.89-105, 1995.

H. Zantema, Termination of String Rewriting Proved Automatically, Journal of Automated Reasoning, vol.33, issue.2, pp.105-139, 2005.
DOI : 10.1007/s10817-005-6545-0

H. Zhang and D. Kapur, First-order theorem proving using conditional rewrite rules, 9th International Conference on Automated Deduction, pp.1-20, 1988.
DOI : 10.1007/BFb0012820

H. T. Zhang and J. Rémy, Contextual rewriting, Proceedings 1st Conference on Rewriting Techniques and Applications, pp.46-62, 1985.
DOI : 10.1007/3-540-15976-2_2