@INPROCEEDINGS{Basinfsttcs00,
AUTHOR = {David Basin and Manuel Clavel and Jos\`e Meseguer},
TITLE = {Rewriting Logic as a Metalogical Framework},
BOOKTITLE = {Foundations of Software Technology and Theoretical Computer Science (FSTTCS)},
Month = {December},
YEAR = 2000,
PAGES = {55-80},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
ABSTRACT      = {
A metalogical framework is a logic with an associated methodology that
is used to represent other logics and to reason about their
metalogical properties.  We propose that logical frameworks can
be good metalogical frameworks when their logics support
reflective reasoning and their theories always have initial models.

We present a concrete realization of this idea in rewriting
logic.  Theories in rewriting logic always have initial
models and this logic supports reflective reasoning.
This implies that inductive reasoning is valid when proving properties
about the initial models of theories in rewriting logic, and
that we can use reflection to reason at the metalevel about these
properties. In fact, we can uniformly reflect induction principles for
proving metatheorems about rewriting logic theories and
their parameterized extensions.  We show that this reflective
methodology provides an effective framework for different, non-trivial,
kinds of formal metatheoretic reasoning; one can, for example, prove
metatheorems that relate theories or establish properties of
parameterized classes of theories. Finally, we report on the
implementation of an inductive theorem prover in the Maude system, whose
design is based on the results presented in this paper.}
}