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-201, 1989.
DOI : 10.1016/0304-3975(89)90003-0

T. Bourdier, H. Cirstea, M. Jaume, and H. Kirchner, On Formal Specification and Analysis of Security Policies, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00429240

H. Bürckert, Matching ??? A special case of unification?, Journal of Symbolic Computation, vol.8, issue.5, pp.523-536, 1989.
DOI : 10.1016/S0747-7171(89)80057-4

H. Comon, Completion of rewrite systems with membership constraints, ICALP, pp.392-403, 1992.
DOI : 10.1007/3-540-55719-9_91

H. Comon and C. Delor, Equational Formulas with Membership Constraints, Information and Computation, vol.112, issue.2, pp.167-216, 1994.
DOI : 10.1006/inco.1994.1056

H. Comon, Tree automata techniques and applications, 2008.

T. Fruhwirth, Logic programs as types for logic programs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.300-309, 1991.
DOI : 10.1109/LICS.1991.151654

J. Goubault-larrecq, The h1 tool suite documentation, 2005.

P. Hinman, Fundamentals of mathematical logic, 2005.

C. Hoot, Completion for constrained term rewriting systems, CTRS, pp.408-423, 1992.
DOI : 10.1007/3-540-56393-8_31

G. Huet, Résolution d'equations dans les langages d'ordre 1, 1976.

G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM, vol.27, issue.4, pp.797-821, 1980.
DOI : 10.1145/322217.322230

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

C. Kirchner, Anti-pattern Matching, ESOP, pp.110-124, 2007.
DOI : 10.1007/978-3-540-71316-6_9
URL : https://hal.archives-ouvertes.fr/inria-00337722

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

F. Nieslon, Normalizable horn clauses, strongly recognizable relations and spi, SAS, pp.20-35, 2002.

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

S. Tison, Tree Automata and Term Rewrite Systems, RTA, pp.27-30, 2000.
DOI : 10.1007/10721975_2