F. Baader and K. Schulz, Uniication in the union of disjoint equational theories, Int. Conference on Automated Deduction, pp.50-65, 1992.

F. Baader and J. Siekmann, Handbook of Logic in Artiicial Intelligence and Logic Programming, chapter Uniication Theory, 1993.

A. Caron, J. Coquide, and M. Dauchet, Encompassment properties and automata with constraints. Int, Conference on Rewriting Techniques and Applications, pp.328-342, 1993.

H. Comon, Completion of rewrite systems with membership constraints, Int. Coll. on Automata, Languages and Programming LNCS, vol.623, 1992.
DOI : 10.1007/3-540-55719-9_91

M. Dalrymple, S. Shieber, and F. Pereira, Ellipsis and higher-order unification, Linguistics and Philosophy, vol.8, issue.1, pp.399-452, 1991.
DOI : 10.1007/BF00630923

C. Gardent and M. Kohlhaase, Higher-order coloured uniication and natural language semantics, Anual Meeting of the ACL, 1996.

W. D. Goldfarb, The undecidability of the second-order unification problem, Theoretical Computer Science, vol.13, issue.2, pp.225-230, 1981.
DOI : 10.1016/0304-3975(81)90040-2

G. Huet, A unification algorithm for typed ??-calculus, Theoretical Computer Science, vol.1, issue.1, pp.27-57, 1975.
DOI : 10.1016/0304-3975(75)90011-0

J. Jaaar, Minimal and complete word uniication, Journal of the ACM, vol.37, issue.1, pp.47-85, 1990.

A. Ko-scielski and L. Pacholski, Complexity of makanin's algorithm, Journal of the ACM, vol.43, issue.4, 1996.

A. Lentin and M. Sch-utzenberger, A combinatorial problem in the theory of free monoids, Conference on Combinatorical Mathematics and its Applications, 1969.

J. Evy, Linear second order uniication. Int, Conference on Rewriting Techniques and Applications, number 1103 of LNCS, 1996.

G. Makanin, The problem of solvability of equations in a free semigroup. Soviet Akad, Nauk SSSR, vol.223, issue.2, 1977.

J. Marcinkowski, Undecidability of the rst order theory of one-step right ground rewriting, Int. Conference on Rewriting Techniques and Applications, 1997.

A. Markov, The theory of algorithms English Translation in Israel Program for Scientiic Translations, Trudy Mat. Inst. Steklov, vol.1, issue.42, 1954.

J. Niehren, M. Pinkal, and P. Ruhrberg, On equality up-to constraints over nite trees, context uniication, and one-step rewriting, 1997. Full version available through WWW from http

J. Niehren, M. Pinkal, and P. Ruhrberg, A uniform approach to underspeciication and parallelism, 1997. Submitted. Available through WWW from http

J. P. Ecuchet, Solutions principales et rang d'un syst??me d'??quations avec constantes dans le mono??de libre, Discrete Mathematics, vol.48, issue.2-3, pp.253-274, 1984.
DOI : 10.1016/0012-365X(84)90187-0

T. Pietrzykowski, A Complete Mechanization of Second-Order Type Theory, Journal of the ACM, vol.20, issue.2, pp.333-364, 1973.
DOI : 10.1145/321752.321764

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

M. Schmidt-schauu, Uniication of stratiied second-order terms, J. W. Goethe Universitt at, 1994.

K. U. Schulz, Word unification and transformation of generalized equations, Journal of Automated Reasoning, vol.7, issue.2, pp.149-184, 1993.
DOI : 10.1007/BF00881904

J. H. Siekmann, String-uniication: Part 1, 1975.

R. Treinen, A new method for undecidability proofs of rst order theories. journal of symbolic computation, pp.437-457, 1992.

R. Treinen, The rst-order theory of one-step rewriting is undecidable, number 1103 in LNCS, pp.276-286, 1996.

S. Tulipani, Decidability of the existential theory of innnite terms with subterm relation, Journal on Information and Computation, vol.103, issue.2, 1993.

K. N. Venkataraman, Decidability of the purely existential fragment of the theory of term algebras, Journal of the ACM, vol.34, issue.2, pp.492-510, 1987.
DOI : 10.1145/23005.24037

S. Vorobyov, The rst-order theory of one step rewriting in linear noetherian systems is undecidable, Int. Conf. on Rewriting Techn. and Appl, 1997.