Internal Strategies in a Reflective Logic

. After introducing the basic notions of reflective logic and internal strategies, we discuss in detail how reflection can be systematically exploited to design a strategy language internal to a reflective logic in the concrete case of rewriting logic and Maude; and we illustrate the advantages of this new approach to strategies by showing how the rules of inference for Knuth-Bendix completion can be given strategies corresponding to completion procedures in a completely modular way, not requiring any change whatsoever to the inference rules themselves. 1 Introduction This paper is part of a long-term effort to study and axiomatize reflective logics and to systematically exploit reflection to bring deduction strategies within the fold of logic. In this way, more powerful, modular, and flexible notions of deduction strategy can be defined and verified. In earlier work [7, 8] we have proposed general axiomatic notions of reflective logic and internal strategy language, and have begun to..