@article{BasinTOCL04,
AUTHOR = {David Basin and Manuel Clavel and Jos\`e Meseguer},
TITLE = "Reflective Metalogical Frameworks",
JOURNAL="ACM Transactions on Computational Logic",
YEAR="2004",
MONTH="July",
VOLUME="5",
NUMBER="3",
PAGES="528--576",
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 theories always
have initial models and they support reflective and parameterized
reasoning.

We develop this thesis both abstractly and concretely.  Abstractly, we
formalize our proposal as a set of requirements and explain how any
logic satisfying these requirements can be used for metalogical
reasoning.  Concretely, we present membership equational logic as a
particular metalogic that satisfies these requirements.  Using
membership equational logic, and its realization in the Maude system, we
show how reflection can be used for different, non-trivial kinds of
formal metatheoretic reasoning. In particular, one can prove
metatheorems that relate theories or establish properties of
parameterized classes of theories.  }, 
NOTE="Tentative."  
}