G. Plotkin, Building-in equational theories, Machine Intelligence, vol.7, pp.73-90, 1972.

F. Baader and J. Siekmann, Unification theory, Handbook of Logic in Artificial Intelligence and Logic Programming, 1993.

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

W. Nutt, P. Réty, and G. Smolka, Basic narrowing revisited, Journal of Symbolic Computation, vol.7, issue.3-4, pp.295-318, 1989.
DOI : 10.1016/S0747-7171(89)80014-8

J. You, Enumerating outer narrowing derivations for constructor-based term rewriting systems, J. Symbolic Computation, vol.73, issue.4, pp.319-342, 1989.

J. Chabin and P. Réty, Narrowing directed by a graph of terms, Proceedings 4th Conference on Rewriting Techniques and Applications, pp.112-123, 1991.
DOI : 10.1007/3-540-53904-2_90

J. J. Moreno-navarro and M. Rodriguez-artalejo, Logic programming with functions and predicates: The language Babel, The Journal of Logic Programming, vol.12, issue.3, pp.191-223, 1992.
DOI : 10.1016/0743-1066(92)90024-W

A. Bockmayr, S. Krischer, and A. Werner, Narrowing strategies for arbitrary canonical systems, Fundamenta Informaticae, vol.24, issue.1 2, pp.125-155, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00074660

A. Antoy, R. Echahed, and M. Hanus, A needed narrowing strategy, Proceedings 21st ACM Symposium on Principle of Programming Languages, pp.268-279, 1994.

J. Burghardt, Regular substitution sets: A means of controlling E-unification, Proceedings 6th Conference on Rewriting Techniques and Applications, pp.382-396, 1995.
DOI : 10.1007/3-540-59200-8_71

R. Gilleron, S. Tison, and M. Tommasi, Some new decidability results on positive and negative set constraints, Proc. First International Conference on Constraints in Computational Logics, pp.336-351, 1994.
DOI : 10.1007/BFb0016864
URL : https://hal.archives-ouvertes.fr/inria-00538880

S. Dumitrescu, G. Paun, and A. Salomaa, Pattern Languages Versus Parallel Communicating Grammar Systems, International Journal of Foundations of Computer Science, vol.08, issue.01, 1996.
DOI : 10.1142/S0129054197000057

Y. Guan, G. Hotz, and A. Reichert, Tree Grammars with Multilinear Interpretation, 1992.

N. Dershowitz and J. Jouannaud, Rewrite Systems, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

D. Kozen, Positive First-Order Logic Is NP-Complete, IBM Journal of Research and Development, vol.25, issue.4, pp.327-332, 1981.
DOI : 10.1147/rd.254.0327

S. Mitra, Semantic Unification for Convergent Rewrite Systems, 1994.

J. Christian, Some termination criteria for narrowing and E-unification, Proceedings 11th International Conference on Automated Deduction, pp.582-588, 1992.

H. Comon, M. Haberstrau, and J. Jouannaud, Syntacticness, Cycle-Syntacticness, and Shallow Theories, Information and Computation, vol.111, issue.1, pp.154-191, 1994.
DOI : 10.1006/inco.1994.1043

R. Nieuwenhuis, Basic paramodulation and decidable theories, Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 1996.
DOI : 10.1109/LICS.1996.561464

D. Kapur and P. Narendran, Matching, unification and complexity, ACM SIGSAM Bulletin, vol.21, issue.4, pp.6-9, 1987.
DOI : 10.1145/36330.36332

S. Mitra, Semantic Unification for Convergent System, 1994.

Y. Kaji, T. Fujiwara, T. S. Kasami, and I. , Solving a Unification Problem under Constrained Substitutions Using Tree Automata, Proceedings of the 14th Conference on FST & TCS, pp.276-287, 1994.
DOI : 10.1006/jsco.1996.0077

H. Faßbender and S. Maneth, A strict border for the decidability of E-unification for recursive functions, Proceedings of the Intern. Conf. on Algebraic and Logic Programming, pp.194-208, 1996.
DOI : 10.1007/3-540-61735-3_13

E. Domenjoud, Combination techniques for non-disjoint equational theories, Proceedings 12th International Conference on Automated Deduction, pp.267-281, 1994.
DOI : 10.1007/3-540-58156-1_19

M. Fernández, Narrowing based procedures for equational disunification, Applicable Algebra in Engineering, Communication and Computing, vol.65, issue.4, pp.1-26, 1992.
DOI : 10.1007/BF01189020

H. Comon, Complete axiomatizations of some quotient term algebras, Theoretical Computer Science, vol.118, issue.2, 1993.

M. Hermann, Overview of Existing Recurrent Schematizations, Proc. of the CADE-13 Workshop on Term Schematization and their Applications, 1996.

A. Amaniss, Classification, extension and applications of some schematization methods of infinite sets of terms, Proc. of the CADE-13 Workshop on Term Schematization and their Applica- tions, 1996.

A. Amaniss, Méthodes de schématisation pour la démonstration automatique, Thèse de, 1996.