G. Bernot, M. Bidoit, and T. Knapik, Behavioural approaches to algebraic specifications, Acta Informatica, vol.19, issue.7, pp.31651-671, 1994.
DOI : 10.1007/BF01177550

A. [. Berregeb, M. Bouhoula, and . Rusinowitch, Observational proofs with critical contexts, Fundamental Approaches to Software Engineering, 1998.
DOI : 10.1007/BFb0053582
URL : https://hal.archives-ouvertes.fr/inria-00098624

R. [. Bauer and . Hennicker, Proving the correctness of algebraic implementations by the ISAR system, DISCO'93, 1993.
DOI : 10.1007/BFb0013164

M. Bidoit and R. Hennicker, Behavioural theories and the proof of behavioural properties, Theoretical Computer Science, vol.165, issue.1, pp.3-55, 1996.
DOI : 10.1016/0304-3975(96)00039-4

A. [. Dennis, I. Bundy, and . Green, Using a generalisation critic to find bisimulations for coinductive proofs, 14th Conference on Automated Deduction, pp.276-290, 1996.
DOI : 10.1007/3-540-63104-6_29

J. Goguen and G. Malcolm, Hidden coinduction: behavioural correctness proofs for objects, Mathematical Structures in Computer Science, vol.9, issue.3, pp.287-319, 1999.
DOI : 10.1017/S0960129599002777

J. Goguen and G. Malcolm, A hidden agenda, Theoretical Computer Science, vol.245, issue.1, pp.55-101, 2000.
DOI : 10.1016/S0304-3975(99)00275-3

J. Guttag, The specification and application to programming of abstract data types, 1975.

M. [. Hennicker and . Bidoit, Observational Logic, Algebraic Methodology and Software Technology, pp.263-277, 1999.
DOI : 10.1007/3-540-49253-4_20

]. R. Hen91 and . Hennicker, Context induction: a proof principle for behavioural abstractions and algebraic implementations, Formal Aspects of Computing, vol.3, issue.4, pp.3-55, 1991.

J. Jouannaud and E. Kounalis, Automatic proofs by induction in theories without constructors, Information and Computation, vol.82, issue.1, pp.1-33, 1989.
DOI : 10.1016/0890-5401(89)90062-X

J. [. Jacobs and . Rutten, A tutorial on coalgebras and coinduction, EATCS Bulletin, vol.62, pp.222-259, 1997.

M. [. Kaplan and . Choquer, On the decidability of quasi-reducibility. Bulletin of European Association for Theoretical Computer Science, 1986.

P. [. Kapur, H. Narendran, and . Zhang, On sufficient-completeness and related properties of term rewriting systems, Acta Informatica, vol.6, issue.5, pp.395-415, 1986.
DOI : 10.1007/BF00292110

]. E. Kou92 and . Kounalis, Testing for the ground (co-)reducibility property in term-rewriting systems, Theoretical Computer Science, vol.106, pp.87-117, 1992.

M. Matsumoto and K. Futatsugi, Test Set Coinduction -- Toward Automated Verification of Behavioural Properties ???, 2nd International Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, 1998.
DOI : 10.1016/S1571-0661(05)80015-5

]. D. Pla85 and . Plaisted, Semantic confluence and completion method. Information and Control, 1985.

]. H. Rei95, An approach to object semantics based on terminal co-algebras, Mathematical Structures in Computer Science, vol.5, pp.129-152, 1995.

R. [. Shmid and . Fettig, Towards an efficient construction of test sets for deciding ground reducibility, 6th Conference on Rewriting Techniques and Applications, 1995.
DOI : 10.1007/3-540-59200-8_49

M. Wirsing, Algebraic specifications, chapter 13, 1990.