General Logics and Logical Frameworks
Narciso Martı́-Oliet, José Meseguer · 1994
Abstract This chapter summarizes a theory of general logics first introduced in [39], in which different aspects, or components, of a logic such as its entailment relation, its proof theory, and its model theory are axiomatized. For the model-theoretic component, the theory of institutions of Goguen and Burstall [24] is adopted. Combinations of several such aspects of a logic are also supported by the theory. Special importance is given to the notion of mapping between logics that preserves the logical structure of some aspect, such as the entailment relation, or the satisfaction relation for the models. Such maps play for logics a role analogous to that played by group homomorphisms for groups. The notion of a logical framework, understood as a logic :ℱ in which many other logics can be represented, is then expressed in terms of appropriate representation maps ℒ →ℱ. The particular logical framework provided by rewriting logic [40] is introduced and discussed, and some of its good properties for representing logics and for reflecting aspects of its own metatheory are explained.