Abstract: Rewriting Logic as a Metalogical Framework David Basin and Manuel Clavel and Josè Meseguer A metalogical framework is a logic with an associated methodology thatis used to represent other logics and to reason about theirmetalogical properties. We propose that logical frameworks canbe good metalogical frameworks when their logics supportreflective reasoning and their theories always have initial models.We present a concrete realization of this idea in rewritinglogic. Theories in rewriting logic always have initialmodels and this logic supports reflective reasoning.This implies that inductive reasoning is valid when proving propertiesabout the initial models of theories in rewriting logic, andthat we can use reflection to reason at the metalevel about theseproperties. In fact, we can uniformly reflect induction principles forproving metatheorems about rewriting logic theories andtheir parameterized extensions. We show that this reflectivemethodology provides an effective framework for different, non-trivial,kinds of formal metatheoretic reasoning; one can, for example, provemetatheorems that relate theories or establish properties ofparameterized classes of theories. Finally, we report on theimplementation of an inductive theorem prover in the Maude system, whosedesign is based on the results presented in this paper.