| Abstract / Kurzbeschreibung: |
For the specification of abstract data types, quite a number of
logical systems have been developed. In this work, we will try to
give an overview over this variety. As a prerequisite, we first study
notions of representation and embedding between logical systems,
which are formalized as institutions here. Different kinds of
representations will lead to a looser or tighter connection of the
institutions, with more or less good possibilities of faithfully
embedding the semantics and of re-using proof support.
In the second part, we then perform a detailed ``empirical'' study of
the relations among various well-known institutions of total,
order-sorted and partial algebras and first-order structures (all with
Horn style, i.e. universally quantified conditional, axioms). We thus
obtain a graph of institutions, with different kinds of edges
according to the different kinds of representations between institutions
studied in the first part.
We also prove some separation results, leading to a hierarchy of
institutions, which in turn naturally leads to five subgraphs of the
above graph of institutions. They correspond to five different levels
of expressiveness in the hierarchy, which can be characterized by
different kinds of conditional generation principles.
We introduce a systematic notation for institutions of total,
order-sorted and partial algebras and first-order structures. The
notation closely follows the combination of features that are present
in the respective institution. This raises the question whether these
combinations of features can be made mathematically precise in some
way. In the third part, we therefore study the combination of
institutions with the help of so-called parchments (which are certain
algebraic presentations of institutions) and parchment morphisms.
|
