After giving general metalogical axioms characterizing reflection in general logics in terms of the notion of a universal theory, this paper specifies a finitely presented universal theory for rewriting logic and gives a detailed proof of the claim made in (Meseguer and Clavel, 1996 (Proc. Reflection'96) that rewriting logic is reflective. The paper also gives general axioms for the notion of a strategy language internal to a given logic. Exploiting the fact that rewriting logic is reflexive, a general method for defining internal strategy languages for it and proving their correctness is proposed and is illustrated with an example. The Maude language has been used as an experimental vehicle for the exploration of these techniques. They seem quite promising for applications such as metaprogramming and module composition, logical framework representations, development of formal programming and proving environments, supercompilation, and formal verification of strategies.
(BibTeX entry) (gzip'ed Postscript)