H. Bürckert, Solving disequations in equational theories, Proc. 9th Conf. on Automated Deduction, pp.517-526, 1988.
DOI : 10.1007/BFb0012853

A. Colmerauer, An introduction to Prolog III, Communication of the ACM, vol.33, issue.7, pp.68-90, 1990.
DOI : 10.1007/978-3-642-76274-1_2

A. Colmerauer, Equations and disequations on finite and infinite trees Proceeding of the International conference on the fifth generation of computer systems Tokyo, pp.85-99, 1984.

A. Colmerauer, Prolog and infinite trees, Logic Programming, pp.231-251, 1982.

A. Colmerauer, . Dao, and . Tbh, Expressiveness of Full First Order Constraints in the Algebra of Finite or Infinite Trees, Constraints, vol.8, issue.3, pp.283-302, 2003.
DOI : 10.1007/3-540-45349-0_14
URL : https://hal.archives-ouvertes.fr/hal-00144924

H. Comon, Unification et disunification : Théorie et applications, 1988.

H. Comon, Résolution de contraintes dans des algèbres de termes. Rapport d'Habilitation, 1992.

B. Courcelle, Equivalences and transformations of regular systems???Applications to recursive program schemes and grammars, Theoretical Computer Science, vol.42, pp.1-122, 1986.
DOI : 10.1016/0304-3975(86)90050-2

T. Dao, Résolution de contraintes du premier ordre dans la théorie des arbres finis ou infinis, Thèse d'informatique, 2000.

K. Djelloul, About the Combination of Trees and Rational Numbers in a Complete First-Order Theory, 5th Int. Conf. FroCoS 2005, LNAI, pp.106-122
DOI : 10.1007/11559306_6

G. Huet, Résolution d'équations dans les langages d'ordre 1, Thèse d'Etat, 1976.

J. Jaffar, Efficient unification over infinite terms, New Generation Computing, vol.22, issue.2, pp.207-219, 1984.
DOI : 10.1007/BF03037057

K. Kunen, Negation in logic programming, The Journal of Logic Programming, vol.4, issue.4, pp.289-308, 1987.
DOI : 10.1016/0743-1066(87)90007-0

M. Maher, Complete axiomatizations of the algebras of finite, rational and infinite trees, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, 1988.
DOI : 10.1109/LICS.1988.5132

A. Malcev, Axiomatizable classes of locally free algebras of various types The Metamathematics of Algebraic Systems. Anatolii Ivanovic Malcev. Collected Papers : 1936-1967, pp.262-281, 1971.

A. Matelli and U. Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems, vol.4, issue.2, pp.258-282, 1982.
DOI : 10.1145/357162.357169

M. Paterson and N. Wegman, Linear unification, Journal of Computer and System Sciences, vol.16, issue.2, pp.158-167, 1978.
DOI : 10.1016/0022-0000(78)90043-0
URL : http://doi.org/10.1016/0022-0000(78)90043-0

V. Ramachandran and P. Van-hentenryck, Incremental algorithms for constraint solving and entailment over rational trees, Proc. of the 13th Conf. Foundations of Software Technology and Theoretical Computer Science, pp.205-217, 1993.
DOI : 10.1007/3-540-57529-4_54

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

S. Vorobyov, An improved lower bound for the elementary theories of trees, Proceeding of the 13th International Conference on Automated Deduction (CADE'96). LNAI 1104, pp.275-287, 1996.
DOI : 10.1007/3-540-61511-3_91