N. Martí-oliet and J. Meseguer, Rewriting logic: roadmap and bibliography, Theoretical Computer Science, vol.285, issue.2, pp.121-154, 2002.
DOI : 10.1016/S0304-3975(01)00357-7

J. Meseguer, P. C. Ölveczky, M. O. Stehr, and C. L. Talcott, Maude as a wide-spectrum framework for formal modeling and analysis of active networks, Proceedings DARPA Active Networks Conference and Exposition, pp.494-510, 2002.
DOI : 10.1109/DANCE.2002.1003516

S. Eker, M. Knapp, K. Laderoute, P. Lincoln, J. Meseguer et al., PATHWAY LOGIC: SYMBOLIC ANALYSIS OF BIOLOGICAL SIGNALING, Biocomputing 2002, pp.400-412, 2002.
DOI : 10.1142/9789812799623_0038

J. Meseguer and G. Rosu, The rewriting logic semantics project, Theoretical Computer Science, vol.373, issue.3, pp.213-237, 2007.
DOI : 10.1016/j.tcs.2006.12.018

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., All About Maude, A High-Performance Logical Framework, Lecture Notes in Computer Science, vol.4350, 2007.

P. Borovanský, C. Kirchner, H. Kirchner, P. E. Moreau, and C. Ringeissen, An Overview of ELAN, Electronic Notes in Theoretical Computer Science, vol.15, 1998.
DOI : 10.1016/S1571-0661(05)82552-6

R. Diaconescu and K. Futatsugi, Logical foundations of CafeOBJ, Theoretical Computer Science, vol.285, issue.2, pp.289-318, 2002.
DOI : 10.1016/S0304-3975(01)00361-9

J. Meseguer, Membership algebra as a logical framework for equational specification, Lecture Notes in Computer Science, vol.1376, pp.18-61, 1997.
DOI : 10.1007/3-540-64299-4_26

S. Eker, J. Meseguer, and A. Sridharanarayanan, The Maude LTL Model Checker, Electronic Notes in Theoretical Computer Science, vol.71, 2002.
DOI : 10.1016/S1571-0661(05)82534-4

J. Meseguer, M. Palomino, and N. Martí-oliet, Equational Abstractions, Lecture Notes in Computer Science, vol.2741, pp.2-16, 2003.
DOI : 10.1007/978-3-540-45085-6_2

M. Clavel, M. Palomino, and A. Riesco, Introducing the ITP tool : a tutorial, J. Universal Computer Science, vol.12, issue.11, pp.1618-1650, 2006.

R. Bruni and J. Meseguer, Semantic foundations for generalized rewrite theories, Theoretical Computer Science, vol.360, issue.1-3, pp.386-414, 2006.
DOI : 10.1016/j.tcs.2006.04.012

J. Meseguer and P. Thati, Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols, WRLA, 2004.

K. Futatsugi, Verifying Specifications with Proof Scores in CafeOBJ, 21st IEEE/ACM International Conference on Automated Software Engineering (ASE'06), pp.3-10, 2006.
DOI : 10.1109/ASE.2006.73

K. Ogata and K. Futatsugi, State Machines as Inductive Types, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, vol.90, issue.12, pp.90-2985, 2007.
DOI : 10.1093/ietfec/e90-a.12.2985

W. Kong, T. Seino, K. Futatsugi, and K. Ogata, A lightweight integration of theorem proving and model checking for system verification, 12th Asia-Pacific Software Engineering Conference (APSEC'05), pp.59-66, 2005.
DOI : 10.1109/APSEC.2005.9

K. Ogata, M. Nakano, M. Nakamura, and K. Futatsugi, Chocolat/SMV: A Translator from CafeOBJ into SMV, Sixth International Conference on Parallel and Distributed Computing Applications and Technologies (PDCAT'05), pp.416-420, 2005.
DOI : 10.1109/PDCAT.2005.98

M. Nakamura, W. Kong, K. Ogata, and K. Futatsugi, A Specification Translation from Behavioral Specifications to Rewrite Specifications, IEICE Transactions on Information and Systems, vol.91, issue.5, pp.91-1492, 2008.
DOI : 10.1093/ietisy/e91-d.5.1492

Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar, Symbolic model checking with rich assertional languages, Theoretical Computer Science, vol.256, issue.1-2, pp.93-112, 2001.
DOI : 10.1016/S0304-3975(00)00103-1

A. Pnueli, J. Xu, and L. Zuck, Liveness with (0,1, ???)- Counter Abstraction, Lecture Notes in Computer Science, pp.107-122, 2002.
DOI : 10.1007/3-540-45657-0_9

. Preuve, Par induction sur la longueur de la réécriture close R ? ?(t) ?? t ? correspondant à R ?? t ?? t ? (cf. définition 3)