zbMATH — the first resource for mathematics

General logics and logical frameworks. (English) Zbl 0817.03005
Gabbay, D. M. (ed.), What is a logical system? Oxford: Oxford University Press. Stud. Log. Comput. 4, 355-391 (1994).
Summary: This paper summarizes a theory of general logics, introduced by the second author [Logic colloq. ’87, Proc. Colloq., Granada/Spain 1987, Stud. Logic Found. Math. 129, 275-329 (1989; Zbl 0691.03001)], 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 J. A. Goguen and R. M. Burstall [J. Assoc. Comput. Mach. 39, No. 1, 95- 146 (1992; Zbl 0799.68134)] is adopted. Combinations of several such aspects of a logic are also supported by the theory. Special attention is given to the notion of mapping between logics that preserves the logical structure of some aspects, 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 \(\mathcal F\) in which many other logics can be represented, is then expressed in terms of appropriate representation maps \({\mathcal L}\to {\mathcal F}\). The particular logical framework provided by rewriting logic [the second author, Theor. Comput. Sci. 96, No. 1, 73-155 (1992; Zbl 0758.68043)] is introduced and discussed, and some of its good properties for representing logics and for reflecting aspects of its own metatheory are explained.
For the entire collection see [Zbl 0811.00005].

03B22 Abstract deductive systems
03C95 Abstract model theory
68Q42 Grammars and rewriting systems
03B80 Other applications of logic
68Q55 Semantics in the theory of computing