A. Bouhoula, Automated Theorem Proving by Test Set Induction, Journal of Symbolic Computation, vol.23, issue.1, pp.47-77, 1997.
DOI : 10.1006/jsco.1996.0076
URL : https://hal.archives-ouvertes.fr/inria-00074196

A. Bouhoula and F. Jacquemard, Verifying regular trace properties of security protocols with explicit destructors and implicit induction, Proc. of the workshop FCS-ARSPA, pp.27-44, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00579015

A. Bouhoula and F. Jacquemard, Automated Induction with Constrained Tree Automata
DOI : 10.1007/978-3-540-71070-7_44
URL : https://hal.archives-ouvertes.fr/inria-00579004

A. Bouhoula and J. Jouannaud, Automata-Driven Automated Induction, Information and Computation, vol.169, issue.1, pp.1-22, 2001.
DOI : 10.1006/inco.2001.3036
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.8766

A. Bouhoula, J. Jouannaud, and J. Meseguer, Specification and proof in membership equational logic, Theoretical Computer Science, vol.236, issue.1-2, pp.35-132, 2000.
DOI : 10.1016/S0304-3975(99)00206-6
URL : https://hal.archives-ouvertes.fr/inria-00099079

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

H. Comon, Unification et disunification. Théories et applications, 1988.
URL : https://hal.archives-ouvertes.fr/tel-00331263

H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, C. Löding et al., Tree automata techniques and applications, 2007.

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-lundh, Handbook of Automated Reasoning, chapter Inductionless Induction . Number chapter 14, 2001.

H. Comon-lundh, F. Jacquemard, and N. Perrin, Tree Automata with Memory, Visibility and Structural Constraints, Proc. of the 10th Int. Conf. on Found. of Software Science and Comp. Struct. (FoSSaCS'07), pp.168-182, 2007.
DOI : 10.1007/978-3-540-71389-0_13
URL : https://hal.archives-ouvertes.fr/inria-00579009

J. Davis, Finite set theory based on fully ordered lists Sets Library Website, 5th International Workshop on the ACL2 Theorem Prover and Its Applications, 2004.

N. Dershowitz and J. Jouannaud, Rewrite systems. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, pp.243-320, 1990.

F. Jacquemard, M. Rusinowitch, and L. Vigneron, Tree automata with equality constraints modulo equational theories, Journal of Logic and Algebraic Programming, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00579011

D. Kapur, Constructors can be partial too, Essays in Honor of Larry Wos, 1997.

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

S. Stratulat, A General Framework to Build Contextual Cover Set Induction Provers, Journal of Symbolic Computation, vol.32, issue.4, pp.403-445, 2001.
DOI : 10.1006/jsco.2000.0469
URL : https://hal.archives-ouvertes.fr/inria-00100927

H. Zhang, Implementing contextual rewriting, Proc. 3rd Int. Workshop on Conditional Term Rewriting Systems, 1992.
DOI : 10.1007/3-540-56393-8_28