L. Bachmair, Proof by consistency in equational theories, Proceedings of the third IEEE Symposium on Logic in Computer Science, pp.228-233, 1988.

A. Bouhoula, Preuves automatiques par r ecurrence dans les th eories conditionnelles. T h ese, 1994.

A. Bouhoula, E. Kounalis, and M. Rusinowitch, Spike: an automatic theorem prover, INRIA, 1992.

R. S. and J. S. Moore, A c omputational Logic Handbook, 1988.

C. Bishcop, W. A. Brock, and . Hunt, Report on the formal speciication and partial speciication on the viper, Computational Logic, vol.46, 1990.

C. Cornes, J. Courant, J. Filli^-atre, G. Huet, P. Manoury et al., The Coq Proof Assistant Reference Manual Version 5, INRIA, vol.10, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00069994

, Explicitation de preuves par r ecurrence implicite. M emoire de DEA (Unpublished), 1994.

L. Fribourg, A strong restriction of the inductive completion procedure, Proceedings 13th International Colloquium on Automata, Languages and Programming, v olume 226 of LNCS, pp.105-115, 1986.

G. Huet and J. Hullot, Proofs by induction in equational theories with constructors, Journal of Computer and System Sciences, vol.25, issue.2, pp.239-266, 1982.
URL : https://hal.archives-ouvertes.fr/inria-00076533

G. Huet, G. Kahn, and C. Paulin-mohring, The Coq Proof Assistant , A T utorial, INRIA, 1995.

. Wa-r-r-e-n-a-.-h-u-n-t, System veriication, Journal of automated r easoning, vol.5, issue.4, 1989.

J. Jouannaud and E. Kounalis, Proof by induction in equational theories without constructors, Proceedings of the rst IEEE Symposium on Logic in Computer Science, vol.358, 1986.

M. Kaufmann, An extension of the boyer-moore theorem prover to support rst-order quantiication, Journal of Automated R easoning, vol.9, pp.355-372, 1992.

E. Kounalis and M. Rusinowitch, A mechanization of conditional reasoning, First International Symposium on Artiicial Intelligence and Mathematics, 1990.

E. Kounalis and M. Rusinowitch, Mechanizing inductive reasoning, Proceedings of the American Association for Artiicial Intelligence Conference, pp.240-245, 1990.

Z. Luo and R. Pollack, Lego proof development system: User's manual, 1992.

L. Magnusson, The new implementation of alf, Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp.1-9

U. S. Reddy, T erm rewriting induction, Proceedings 10th International Conference o n A utomated D e duction, vol.162, 1990.

H. Zhang, D. Kapur, and M. S. Krishnamoorthy, A mechanizable induction principle for equational speciications, Proceedings 9th International Conference o n A utomated D e duction, vol.162, 1988.
DOI : 10.1007/bfb0012831