@Article{ basin.ea:reflective:2004, abstract = {A metalogical framework is a logic with anassociated methodology that is used to represent other logics and toreason about their metalogical properties. We propose that logicalframeworks can be good metalogical frameworks when their theories alwayshave initial models and they support reflective and parameterizedreasoning.We develop this thesis both abstractly and concretely. Abstractly, weformalize our proposal as a set of requirements and explain how anylogic satisfying these requirements can be used for metalogicalreasoning. Concretely, we present membership equational logic as aparticular metalogic that satisfies these requirements. Usingmembership equational logic, and its realization in the Maude system, weshow how reflection can be used for different, non-trivial kinds offormal metatheoretic reasoning. In particular, one can provemetatheorems that relate theories or establish properties ofparameterized classes of theories.}, author = {David Basin and Manuel Clavel and Jos\`e Meseguer}, copyright = {Copyright © 2004 ACM, Inc.}, copyrighturl = {http://portal.acm.org/citation.cfm?doid=1013560.1013566}, issn = { ISSN:1529-3785}, journal = {ACM Transactions on Computational Logic}, language = {USenglish}, month = {July}, number = 3, pages = {528--576}, title = {Reflective Metalogical Frameworks}, volume = 5, year = 2004, user = {bgeiser} }