The Institution of Order-Sorted Equational Logic.
Grigore Roşu · 1994
The paper provides an organisation of order-sorted equational logic as an Institution. 1 Introduction It is well known that Institution are a very strong tool for abstract model theory. Among many other models, order-sorted logic proved itself as a particularily useful formalism for logic-based programming. It is, therefore, important to include it into a general frame, where powerful methods are available. This paper organizes order-sorted equational logic as an Institution. For all the necesary background from category theory and many-sorted algebra, the reader is referred to [2]. 2 Preliminaries In the following we will present the basic conventions and notations we are dealing with. Let S be a "sort set". An S-sorted set A is just a family of sets A s for every sort s 2 S; we will write fA s j s 2 Sg. Similarly, given S-sorted sets A and B, an S-sorted function f : A ! B is an S-sorted family ff s : A s ! b s j s 2 Sg. If f : A ! B and g : B ! C are two S-sorted functions then ...