M. Aiguier, A. Arnould, C. Boin, P. L. Gall, and B. Marre, Testing from Algebraic Specifications: Test Data Set Selection by Unfolding Axioms, Formal Approaches to Testing of Software (FATES), pp.304-317, 2005.
DOI : 10.1109/ASE.2000.873667
URL : https://hal.archives-ouvertes.fr/hal-00341963

M. Aiguier, A. Arnould, P. L. Gall, and D. Longuet, Test Selection Criteria for Quantifier-Free First-Order Specifications, International Symposium on Fundamentals of Software ENgineering (FSEN), pp.144-160, 2007.
DOI : 10.1007/978-3-540-75698-9_10
URL : https://hal.archives-ouvertes.fr/hal-00353787

M. Aiguier and D. Bahrami, Structures for Abstract Rewriting, Journal of Automated Reasoning, vol.28, issue.1-2, pp.303-351, 2007.
DOI : 10.1007/s10817-006-9065-7
URL : https://hal.archives-ouvertes.fr/hal-00341965

M. Aiguier, D. Bahrami, and C. Dubois, On a Generalised Logicality Theorem, Artificial Intelligence, Automated Reasoning, and Symbolic Computation, pp.51-64, 2002.
DOI : 10.1007/3-540-45470-5_8

M. Aiguier and F. Barbier, An Institution-independent Proof of the Beth Definability Theorem, Studia Logica, vol.53, issue.5, pp.333-359, 2007.
DOI : 10.1007/s11225-007-9043-z
URL : https://hal.archives-ouvertes.fr/hal-00341967

M. Aiguier and R. Diaconescu, Stratified institutions and elementary homomorphisms, Information Processing Letters, vol.103, issue.1, pp.5-13, 2007.
DOI : 10.1016/j.ipl.2007.02.005
URL : https://hal.archives-ouvertes.fr/hal-00341974

M. Aiguier and D. Longuet, Test Selection Criteria for Modal Specifications of Reactive Systems, First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), pp.159-170, 2007.
DOI : 10.1109/TASE.2007.52

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

N. D. Belnap, Display logic, Journal of Philosophical Logic, vol.11, issue.4, pp.375-417, 1982.
DOI : 10.1007/BF00284976

U. Berger, M. Eberl, and H. Schwichtenberg, Term rewriting for normalization by evaluation, Information and Computation, vol.183, issue.1, pp.19-42, 2003.
DOI : 10.1016/S0890-5401(03)00014-2

G. Birkhoff, On the structure of abstract algebras, Proceedings of The Cambridge Philosophical Society, pp.433-454, 1935.

E. and T. Bittar, Strong normalization proofs for cut-elimination in Gentzen's sequent calculi, Proceedings of the Symposium on Algebra and Computer Science, pp.179-225, 1999.

T. Borzyszkowski, Logical systems for structured specifications, Theoretical Computer Science, vol.286, issue.2, pp.197-245, 2002.
DOI : 10.1016/S0304-3975(01)00317-6

E. Cichon, M. Rusinowitch, and S. Selhab, Cut elimination and rewriting: termination proofs, 1996.

C. Cornes, J. Courant, J. Fillâtre, G. Huet, P. Manoury et al., The Coq proof assistant reference manual, version 5.10, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00069994

J. Dawson and R. Gore, A New Machine-checked Proof of Strong Normalisation for Display Logic, Electronic Notes in Theoretical Computer Science, 2003.
DOI : 10.1016/S1571-0661(04)81004-1

J. Dawson and R. Goré, A General Theorem on Termination of Rewriting, In Computer Science Logic Lecture Notes in Computer Science, vol.3210, pp.100-114, 2004.
DOI : 10.1007/978-3-540-30124-0_11

J. Dawson and R. Goré, Termination of abstract reduction systems computing In The Australian Theory Symposium, of Conferences in Research and Practice in Information Technology (CRPIT), pp.35-43, 2007.

N. Dershowitz, A note on simplification orderings, Information Processing Letters, vol.9, issue.5, pp.212-215, 1979.
DOI : 10.1016/0020-0190(79)90071-1

N. Dershowitz and J. Jouannaud, Rewrite Systems, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

N. Dershowitz and C. Kirchner, Abstract saturation-based inference, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., 2003.
DOI : 10.1109/LICS.2003.1210046
URL : https://hal.archives-ouvertes.fr/inria-00099466

N. Dershowitz and C. Kirchner, Abstract canonical presentations, Theoretical Computer Science, vol.357, issue.1-3, pp.53-69, 2006.
DOI : 10.1016/j.tcs.2006.03.012
URL : https://hal.archives-ouvertes.fr/inria-00121760

R. Diaconescu, Institution-independent Model Theory, Studies in Universal Logic. Birkhuser, 2008.
DOI : 10.1007/11780274_5

R. Diaconescu, J. Goguen, and P. Stefaneas, Logical support for modularization, Logical Environments Proceedings of Workshop on Logical Frameworks, pp.83-130, 1991.

G. Dowek, Confluence as a Cut Elimination Property, Rewriting Techniques and Applications, pp.2-14, 2003.
DOI : 10.1007/3-540-44881-0_2
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.2708

G. Dowek, . Th, C. Hardin, and . Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506

G. Dowek and B. Werner, An inconsistent theory modulo defined by a confluent and terminating rewrite system

G. Dowek and B. Werner, Proof normalization modulo, International Workshop on Types for Proofs and Programs, pp.62-77, 1999.
DOI : 10.1007/3-540-48167-2_5
URL : https://hal.archives-ouvertes.fr/inria-00073143

G. Dowek and B. Werner, Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003.
DOI : 10.1007/BFb0037116

A. Dragalin, Mathematical intuitionism, introduction to proof theory Translation of the russian original from, Translations of Mathematical Monographs, vol.67, pp.185-199, 1979.

J. Fiadeiro and A. Sernadas, Structuring theories on consequence, Recent Trends in Algebraic Development Techniques, pp.44-72, 1988.
DOI : 10.1007/3-540-50325-0_3

J. Gallier, Logic for Computer Science, volume Foundations of Automatic Theorem Proving, 1986.

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, The collected Papers of Gerhard Gentzen, pp.176-210405, 1935.
DOI : 10.1007/BF01201353

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, 1989.

J. A. Goguen and R. Burstall, Institutions: abstract model theory for specification and programming, Journal of the ACM, vol.39, issue.1, pp.95-146, 1992.
DOI : 10.1145/147508.147524

H. Herbelin, A ??-calculus structure isomorphic to Gentzen-style sequent calculus structure, Proceedings of the 8th International Workshop on Computer Science Logic, pp.61-75, 1995.
DOI : 10.1007/BFb0022247
URL : https://hal.archives-ouvertes.fr/inria-00381525

O. Hermant, A model-based cut elimination proof, 2nd St-Petersburg Days of Logic and Computability, 2003.

O. Hermant, Semantic Cut Elimination in the Intuitionistic Sequent Calculus, International conference on Typed Lambda Calculi and Applications (TLCA), pp.221-233, 2007.
DOI : 10.1007/11417170_17

S. Kaplan, Conditional rewrite rules, Theoretical Computer Science, vol.33, issue.2-3, pp.175-193, 1984.
DOI : 10.1016/0304-3975(84)90087-2
URL : http://doi.org/10.1016/0304-3975(84)90087-2

S. Kleene, Introduction to Meta-mathematics, 1952.

J. Levy and J. Agustí, Bi-rewrite Systems, Journal of Symbolic Computation, vol.22, issue.3, pp.279-314, 1996.
DOI : 10.1006/jsco.1996.0053
URL : http://doi.org/10.1006/jsco.1996.0053

D. Longuet and M. Aiguier, Specification-Based Testing for CoCasl???s Modal Specifications, Conference on Algebra and Coalgebra in Computer Science (CALCO), pp.356-371, 2007.
DOI : 10.1007/978-3-540-73859-6_24

D. Longuet and M. Aiguier, Integration testing from structured specifications via deduction modulo, International Colloquium on Theoretical Aspects of Computing, 2009.
DOI : 10.1007/978-3-642-03466-4_17
URL : https://hal.archives-ouvertes.fr/hal-00812193

D. Longuet, M. Aiguier, and P. L. Gall, Proof-Guided Test Selection from First-Order Specifications with Equality, Journal of Automated Reasoning, vol.4, issue.2, 2009.
DOI : 10.1007/s10817-009-9128-7
URL : https://hal.archives-ouvertes.fr/hal-00782871

J. Meseguer, General Logics, Logic Colloquium'87, pp.275-329, 1989.
DOI : 10.1016/S0049-237X(08)70132-0

T. Nipkow, L. Paulson, and M. Wenzel, Isabelle's logics: HOL. http

D. Prawitz, Natural deduction: A proof-theoretical study, Almqvist and Wiksell, 1965.

A. Salibra and G. Scollo, Compactness and Löwenheim-Skolem properties in categories of pre-institutions, Algebraic Methods in Logic and in Computer Science, pp.67-94, 1993.

A. Salibra and G. Scollo, Interpolation and compactness in categories of pre-institutions, Mathematical Structures in Computer Science, vol.332, issue.03, pp.261-286, 1996.
DOI : 10.1007/BF01190411

W. and M. Schorlemmer, Term Rewriting in a Logic of Special Relations, 7th International Conference on Algebraic Methodology and Software Technology, pp.178-195, 1998.
DOI : 10.1007/3-540-49253-4_15

G. Struth, Non-symmetric rewriting, 1996.

W. Tait, Normal derivability in classical logic The Syntax and Semantics of Infinitary Languages, pp.204-236, 1989.

A. Tarlecki, On the existence of free models in abstract algebraic institutions, Theoretical Computer Science, vol.37, pp.269-304, 1986.
DOI : 10.1016/0304-3975(85)90094-5

A. Tarlecki, Quasi-varieties in abstract algebraic institutions, Journal of Computer and System Sciences, vol.33, issue.3, pp.269-304, 1986.
DOI : 10.1016/0022-0000(86)90057-7

A. Tarlecki, Algebraic Foundations of Systems Specification, chapter Institutions: An abstract Framework for Formal Specifications IFIP State-of-the-Art Reports, pp.105-131, 1999.

C. Urban and G. Bierman, Strong Normalisation of Cut-Elimination in Classical Logic, Acta Informaticae, vol.45, issue.12, pp.123-155, 2001.
DOI : 10.1007/3-540-48959-2_26

V. Van-oostrom, Sub-Birkhoff, 7th International Symposium on Functional and Logic Programming, pp.180-195, 2004.
DOI : 10.1007/978-3-540-24754-8_14

L. Wallen, Automated Deduction for Non Classical Logics, 1990.

T. Yamada, J. Avenhaus, C. Loria-saenz, and A. Middeldorp, Logicality of conditional rewrite systems, Theoretical Computer Science, vol.236, issue.1-2, pp.209-232, 2000.
DOI : 10.1016/S0304-3975(99)00210-8

M. Aiguier, M. , and ´. Paris, Châtenay-Malabry, France e-mail: marc.aiguier@ecp.fr Delphine Longuet Univ