# Semantics of the Distributed Ontology Language: Institutes and Institutions

Till Mossakowski, Oliver Kutz, Christoph Lange

► To cite this version:

Till Mossakowski, Oliver Kutz, Christoph Lange. Semantics of the Distributed Ontology Language: Institutes and Institutions. 21th International Workshop on Algebraic Development Techniques (WADT), Jun 2012, Salamanca, Spain. pp.212-230, 10.1007/978-3-642-37635-1_13. hal-01485971

HAL Id: hal-01485971

https://inria.hal.science/hal-01485971

Submitted on 9 Mar 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Semantics of the Distributed Ontology Language:
Institutes and Institutions

Till Mossakowski<fnref n="1" />,<fnref n="3" />, Oliver Kutz<fnref n="1" />, and Christoph Lange<fnref n="1" />,<fnref n="2" />

**Abstract.** The Distributed Ontology Language (DOL) is a recent development within the ISO standardisation initiative 17347 Ontology Integration and Interoperability (OntoIOp). In DOL, heterogeneous and distributed ontologies can be expressed, i.e. ontologies that are made up of parts written in ontology languages based on various logics. In order to make the DOL meta-language and its semantics more easily accessible to the wider ontology community, we have developed a notion of institute which are like institutions but with signature partial orders and based on standard set-theoretic semantics rather than category theory. We give an institute-based semantics for the kernel of DOL and show that this is compatible with institutional semantics. Moreover, as it turns out, beyond their greater simplicity, institutes have some further surprising advantages over institutions.

# 1 Introduction

OWL is a popular language for ontologies. Yet, the restriction to a decidable description logic often hinders ontology designers from expressing knowledge that cannot (or can only in quite complicated ways) be expressed in a description logic. A current practice to deal with this problem is to intersperse OWL ontologies with first-order axioms in the comments or annotate them as having temporal behaviour [35, 3], e.g. in the case of bio-ontologies where mereological relations such as parthood are of great importance, though not definable in OWL. However, these remain informal annotations to inform the human designer, rather than first-class citizens of the ontology with formal semantics, and will therefore unfortunately be ignored by tools with no impact on reasoning. Moreover, foundational ontologies such as DOLCE, BFO or SUMO use full first-order logic or even first-order modal logic.

A variety of languages is used for formalising ontologies.<fnref n="4" /> Some of these, such as RDF, OBO and UML, can be seen more or less as fragments and notational variants of OWL, while others, such as F-logic and Common Logic (CL), clearly go beyond the expressiveness of OWL.

This situation has motivated the Distributed Ontology Language (DOL), a language currently under active development within the ISO standard 17347 Ontology Integration and Interoperability (OntoIOp). In DOL, heterogeneous and distributed ontologies can be expressed. At the heart of this approach is a graph of ontology languages and translations [27], shown in Fig. 1.

<footnote n="1">¹ Research Center on Spatial Cognition, University of Bremen</footnote>

<footnote n="2">² School of Computer Science, University of Birmingham</footnote>

<footnote n="3">³ DFKI GmbH Bremen</footnote>

<footnote n="4">⁴ For the purposes of this paper, “ontology” can be equated with “logical theory”.</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1. An initial logic graph for the Distributed Ontology Language DOL</figcaption></figure>

This graph enables users to

- relate ontologies that are written in different formalisms (e.g. prove that the OWL version of the foundational ontology DOLCE is logically entailed by the first-order version);

- re-use ontology modules even if they have been formulated in a different formalism;

- re-use ontology tools such as theorem provers and module extractors along translations between formalisms.

What is the semantics of DOL? Previous presentations of the semantics of heterogeneous logical theories [36, 7, 30, 16, 27] relied heavily on the theory of institutions [10]. The central insight of the theory of institutions is that logical notions such as model, sentence, satisfaction and derivability should be indexed over signatures (vocabularies). In order to abstract from any specific form of signature, category theory is used: nothing more is assumed about signatures other than that (together with suitable signature morphisms) they form a category.

However, the use of category theory diminishes the set of potential readers:

> "Mathematicians, and even logicians, have not shown much interest in the theory of institutions, perhaps because their tendency toward Platonism inclines them to believe that there is just one true logic and model theory; it also doesn't *much help that institutions use category theory extensively.*"

*(J. Goguen and G. Roșu in [9], our emphasis)*

Indeed, during the extensive discussions within the ISO standardisation committee in TC37/SC3 to find an agreement concerning the right semantics for the DOL language, we (a) encountered strong reservations to base the semantics entirely on the institutional
approach in order not to severely limit DOL's potential adoption by users, and (b) re-
alised that a large kernel of the DOL language can be based on a simpler, category-free
semantics. The compromise that was found within OntoIOp therefore adopted a two-
layered approach: (i) it bases the semantics of a large part of DOL on a simplification
of the notion of institutions, namely the institute-based approach presented in this paper
that relies purely on standard set-theoretic semantics, and (ii) allows an elegant addition
of additional features that do require a full institution-based approach.

Indeed, it turned out that the majority of work in the ontology community either disregards signature morphisms altogether, or uses only signature inclusions. The latter are particularly important for the notion of ontology module, which is essentially based on the notion of conservative extension along an inclusion signature morphisms, and related notions like inseparability and uniform interpolation (see also Def. 5 below). Another use case for signature inclusions are theory interpretations, which are used in the COLORE repository of (first-order) Common Logic ontologies. Indeed, COLORE uses the technique of extending the target of a theory interpretation by suitable definitions of the symbols in the source. The main motivation for this is probably the avoidance of derived signature morphisms; as a by-product, also renamings of symbols are avoided.

There are only rare cases where signature morphisms are needed in their full gener-
ality: the renaming of ontologies, which so far has only been used for combinations of
ontologies by colimits. Only here, the full institution-based approach is needed. How-
ever, only relatively few papers are explicitly concerned with colimits of ontologies.<fnref n="5" />

Another motivation for our work is the line of *signature-free* thinking in logic and
ontology research; for example, the ISO/IEC standard 24707:2007 Common Logic [5]
names its signature-free approach to sentence formation a chief novel feature:

> “Common Logic has some novel features, chief among them being a syntax which is *signature-free* ...” [5]

Likewise, many abstract studies of consequence and satisfaction systems [1, 10, 19, 20] disregard signatures. Hence, we base our semantics on the newly introduced notion of *institutes*. These start with the signature-free approach, and then introduce signatures a posteriori, assuming that they form a partial order. While this approach covers only signature inclusions, not renamings, it is much simpler than the category-based approach of institutions. Of course, for features like colimits, full institution theory is needed. We therefore show that institutes and institutions can be integrated smoothly.

## 2 Institutes: Semantics for a DOL Kernel

The notion of institute follows the insight that central to a model-theoretic view on
logic is the notion of satisfaction of sentences in models. We also follow the insight of
institution theory that signatures are essential to control the vocabulary of symbols used
in sentences and models. However, in many logic textbooks as well as in the Com-
mon Logic standard [5], sentences are defined independently of a specific signature,

<footnote n="5">⁵ To make this more explicit, as of January 2013, Google Scholar returns about 1 million papers for the keyword 'ontology', around 10,000 for the keyword 'colimits', but only around 200 for the conjunctive query.</footnote>
while models always interpret a given signature. The notion of institute reflects this common practice. Note that the satisfaction relation can only meaningfully be defined between models and sentences where the model interprets all the symbols occurring in the sentence; this is reflected in the fact that we define satisfaction per signature. We also require a partial order on models; this is needed for minimisation in the sense of circumscription.

Moreover, we realise the goal of avoiding the use of category theory by relying on partial orders of signatures as the best possible approximation of signature categories. This also corresponds to common practice in logic, where signature extensions and (reducts against these) are considered much more often than signature morphisms.

**Definition 1 (Institutes).** An institute $\mathcal{I} = (\mathbf{Sen}, \mathbf{Sign}, \leq, \mathbf{sig}, \mathbf{Mod}, |\cdot|, .)$ consists of

- a class Sen of sentences;

- a partially ordered class (Sign, ≤) of signatures (which are arbitrary sets);

- a function sig : Sen → Sign, giving the (minimal) signature of a sentence (then for each signature Σ, let Sen(Σ) = {φ ∈ Sen | sig(φ) ≤ Σ});

- for each signature Σ, a partially ordered class Mod(Σ) of Σ-models;

- for each signature Σ, a satisfaction relation $|\Sigma| \subseteq \mathbf{Mod}(\Sigma) \times \mathbf{Sen}(\Sigma)$;

- for any Σ₂-model M, a Σ₁-model M|Σ₁ (called the **reduct**), provided that Σ₁ ≤ Σ₂,

such that the following properties hold:

- given Σ₁ ≤ Σ₂, for any Σ₂-model M and any Σ₁-sentence φ

$$M \models \varphi \text{ iff } M|_{\Sigma_1} \models \varphi$$

(satisfaction is **invariant under reduct**),

- for any Σ-model M, given Σ₁ ≤ Σ₂ ≤ Σ,

$$(M|_{\Sigma_2})|_{\Sigma_1} = M|_{\Sigma_1}$$

(reducts are **compositional**), and

- for any Σ-models M₁ ≤ M₂, if Σ' ≤ Σ, then M₁|Σ' ≤ M₂|Σ' (reducts preserve the **model ordering**).

□

We give two examples illustrating these definitions, by phrasing the description logic ALC and Common Logic CL in institute style:

**Example 2 (Description Logics ALC).** An institute for ALC is defined as follows: sentences are subsumption relations $C_1 \subseteq C_2$ between concepts, where concepts follow the grammar

$$C ::= A | \top | \bot | C_1 \sqcup C_2 | C_1 \sqcap C_2 | \neg C | \forall R.C | \exists R.C$$

Here, A stands for atomic concepts. Such sentences are also called TBox sentences. Sentences can also be ABox sentences, which are membership assertions of individuals in concepts (written a : C, where a is an individual constant) or pairs of individuals in roles (written R(a, b), where R is a role, and a, b are individual constants).
Signatures consist of a set $\mathcal{A}$ of atomic concepts, a set $\mathcal{R}$ of roles and a set $\mathcal{I}$ of
individual constants. The ordering on signatures is component-wise inclusion. For a
sentence $\varphi$, $\mathit{sig}(\varphi)$ contains all symbols occurring in $\varphi$.

$\Sigma$-models consist of a non-empty set $\Delta$, the universe, and an element of $\Delta$ for each
individual constant in $\Sigma$, a unary relation over $\Delta$ for each concept in $\Sigma$, and a binary
relation over $\Delta$ for each role in $\Sigma$. The partial order on models is defined as coincidence
of the universe and the interpretation of individual constants plus subset inclusion for
the interpretation of concepts and roles. Reducts just forget the respective components
of models. Satisfaction is the standard satisfaction of description logics.

An extension of *ALC* named *SROIQ* [13] is the logical core of the Web Ontology Language OWL 2 DL<fnref n="6" />.

*Example 3 (Common Logic - CL)*. Common Logic (CL) has first been formalised as an institution in [16]. We here formalise it as an institute.

A CL-sentence is a first-order sentence, where predications and function applica-
tions are written in a higher-order like syntax as $t(s)$. Here, $t$ is an arbitrary term, and
$s$ is a sequence term, which can be a sequence of terms $t_1...t_n$, or a sequence marker.
However, a predication $t(s)$ is interpreted like the first-order formula *holds*($t$, $s$), and a
function application $t(s)$ like the first-order term *app*($t$, $s$), where *holds* and *app* are fic-
titious symbols (denoting the semantic objects *rel* and *fun* defined in models below). In
this way, CL provides a first-order simulation of a higher-order language. Quantification
variables are partitioned into those for individuals and those for sequences.

A CL signature $\Sigma$ (called vocabulary in CL terminology) consists of a set of names, with a subset called the set of discourse names, and a set of sequence markers. The partial order on signatures is componentwise inclusion with the requirement that the a name is a discourse name in the smaller signature if and only if is in the larger signature. *sig* obviously collects the names and sequence markers present in a sentence.

A $\Sigma$-model consists of a set $UR$, the universe of reference, with a non-empty subset $UD \subseteq UR$, the universe of discourse, and four mappings:

- *rel* from *UR* to subsets of *UD*\* = {<x₁, ..., xₙ > | x₁, ..., xₙ ∈ *UD*} (i.e., the set of finite sequences of elements of *UD*);

- *fun* from *UR* to total functions from *UD*\* into *UD*;

- *int* from names in *Σ* to *UR*, such that *int*(*v*) is in *UD* if and only if *v* is a discourse name;

- *seq* from sequence markers in *Σ* to *UD*\*.

The partial order on models is defined as $M_1 \leq M_2$ iff $M_1$ and $M_2$ agree on all components except perhaps *rel*, where we require $rel_1(x) \subseteq rel_2(x)$ for all $x \in UR_1 = UR_2$. Model reducts leave *UR*, *UD*, *rel* and *fun* untouched, while *int* and *seq* are restricted to the smaller signature.

Interpretation of terms and formulae is as in first-order logic, with the difference
that the terms at predicate resp. function symbol positions are interpreted with *rel* resp.
*fun* in order to obtain the predicate resp. function, as discussed above. A further differ-
ence is the presence of sequence terms (namely sequence markers and juxtapositions

<footnote n="6">⁶ See also http://www.w3.org/TR/owl2-overview/</footnote>
of terms), which denote sequences in UD*, with term juxtaposition interpreted by sequence concatenation. Note that sequences are essentially a second-order feature. For details, see [5].

**Working within an arbitrary but fixed Institute**

Like with institutions, many logical notions can be formulated in an arbitrary but fixed institute. However, institutes are more natural for certain notions used in the ontology community.

The notions of ‘theory’ and ‘model class’ in an institute are defined as follows:

**Definition 4 (Theories and Model Classes).** A *theory* $T = (\Sigma, \Gamma)$ *in an institute* $\mathcal{I}$
*consists of a signature* $\Sigma$ *and a set of sentences* $\Gamma \subseteq \text{Sen}(\Sigma)$. *Theories can be partially*
*ordered by letting* $(\Sigma_1, \Gamma_1) \le (\Sigma_2, \Gamma_2)$ *iff* $\Sigma_1 \subseteq \Sigma_2$ *and* $\Gamma_1 \subseteq \Gamma_2$. *The *class of models*
*Mod*(Σ, Γ) *is defined as the class of those* Σ-models satisfying Γ. *This data is easily*
*seen to form an institute* $\mathcal{I}^\text{th}$ *of theories in* $\mathcal{I}$ *(with theories as “signatures”).* $\square$

The following definition is taken directly from [21],<fnref n="7" /> showing that central notions
from the ontology modules community can be seamlessly formulated in an arbitrary
institute:

**Definition 5 (Entailment, inseparability, conservative extension).**

- A theory $T_1 \Sigma$-entails $T_2$, written $T_1 \subseteq T_2$, if $T_2 \models \varphi$ implies $T_1 \models \varphi$ for all sentences $\varphi$ with $sig(\varphi) \le \Sigma$;

- $T_1$ and $T_2$ are $\Sigma$-inseparable if $T_1 \Sigma$-entails $T_2$ and $T_2 \Sigma$-entails $T_1$;

- $T_2$ is a $\Sigma$-conservative extension of $T_1$ if $T_2 \ge T_1$ and $T_1$ and $T_2$ are $\Sigma$-inseparable;

- $T_2$ is a conservative extension of $T_1$ if $T_2$ is a $\Sigma$-conservative extension of $T_2$ with $\Sigma = sig(T_1)$.

Note the use of *sig* here directly conforms to institute parlance. In contrast, since there is
no global set of sentences in institutions, one would need to completely reformulate the
definition for the institution representation and fiddle with explicit sentence translations.

From time to time, we will need the notion of ‘unions of signatures’:

**Definition 6 (Signature unions).** A *Signature union* is a supremum (least upper bound) in the signature partial order. Note that signature unions need not always exist, nor be unique. In either of these cases, the enclosing construct containing the union is *unde-fined*. □

<footnote n="7">⁷ There are two modifications: 1. We use $\le$ where [21] write $\subseteq$. 2. In [21], all these notions are defined relative to a query language. This can also be done in an institute by singling out a subinstitute (see end of Sect. 3 below), which then becomes an additional parameter of the definition.</footnote>
### 3 Institute Morphisms and Comorphisms

Institute morphisms and comorphisms relate two given institutes. A typical situation is that an institute morphism expresses the fact that a "larger" institute is built upon a "smaller" institute by projecting the "larger" institute onto the "smaller" one. Somewhat dually to institute morphisms, institute comorphisms allow to express the fact that one institute is included in another one. (Co)morphisms play an essential role for DOL: the DOL semantics is parametrised over a graph of institutes and institute morphisms and comorphisms. The formal definitions are as follows:

**Definition 7 (Institute morphism).** Given $\mathcal{I}_1 = (\mathbf{Sen}_1, \mathbf{Sign}_1, \leq_1, \mathrm{sig}_1, \mathbf{Mod}_1, |\models, |.)$ and $\mathcal{I}_2 = (\mathbf{Sen}_2, \mathbf{Sign}_2, \leq_2, \mathrm{sig}_2, \mathbf{Mod}_2, |\models, |.)$, an institute morphism $\rho = (\Phi, \alpha, \beta): \mathcal{I}_1 \to \mathcal{I}_2$ consists of

- a monotone map $\Phi : (\mathbf{Sign}^1, \leq^1) \to (\mathbf{Sign}^2, \leq^2)$,

- a sentence translation function $\alpha : \mathbf{Sen}_2 \to \mathbf{Sen}_1$, and

- for each $\mathcal{I}_1$-signature $\Sigma$, a monotone model translation function $\beta_\Sigma : \mathbf{Mod}_1(\Sigma) \to \mathbf{Mod}_2(\Phi(\Sigma))$,

such that

- $M_1 \models_1 \alpha(\varphi_2)$ if and only if $\beta_\Sigma(M_1) \models_2 \varphi_2$ holds for each $\mathcal{I}_1$-signature $\Sigma$, each model $M_1 \in \mathbf{Mod}_1(\Sigma)$ and each sentence $\varphi_2 \in \mathbf{Sen}_2(\Sigma)$ (satisfaction condition)

- $\Phi(\mathrm{sig}^1(\alpha(\varphi_2))) \leq \mathrm{sig}^2(\varphi_2)$ for any sentence $\varphi_2 \in \mathbf{Sen}_2$ (sentence coherence);

- model translation commutes with reduct, that is, given $\Sigma_1 \leq \Sigma_2$ in $\mathcal{I}_1$ and a $\Sigma_2$-model $M$,

$$ \beta_{\Sigma_2}(M)|_{\Phi(\Sigma_1)} = \beta_{\Sigma_1}(M|_{\Sigma_1}). $$

□

The dual notion of institute comorphism is then defined as:

**Definition 8 (Institute comorphism).** Given $\mathcal{I}_1 = (\mathbf{Sen}_1, \mathbf{Sign}_1, \leq_1, \mathrm{sig}_1, \mathbf{Mod}_1, |\models, |.)$ and $\mathcal{I}_2 = (\mathbf{Sen}_2, \mathbf{Sign}_2, \leq_2, \mathrm{sig}_2, \mathbf{Mod}_2, |\models, |.)$, an institute comorphism $\rho = (\Phi, \alpha, \beta): \mathcal{I}_1 \to \mathcal{I}_2$ consists of

- a monotone map $\Phi : (\mathbf{Sign}^1, \leq^1) \to (\mathbf{Sign}^2, \leq^2)$,

- a sentence translation function $\alpha : \mathbf{Sen}_1 \to \mathbf{Sen}_2$, and

- for each $\mathcal{I}_1$-signature $\Sigma$, a monotone model translation function $\beta_\Sigma : \mathbf{Mod}_2(\Phi(\Sigma)) \to \mathbf{Mod}_1(\Sigma)$,

such that

- $M_2 \models_2 \alpha(\varphi_1)$ if and only if $\beta_\Sigma(M_2) \models_1 \varphi_1$ holds for each $\mathcal{I}_1$-signature $\Sigma$, each model $M_2 \in \mathbf{Mod}_2(\Sigma)$ and each sentence $\varphi_1 \in \mathbf{Sen}_1(\Sigma)$ (satisfaction condition)

- $\mathrm{sig}_2(\alpha(\varphi_1)) \leq \Phi(\mathrm{sig}_1(\varphi_1))$ for any sentence $\varphi_1 \in \mathbf{Sen}_1$ (sentence coherence);

- model translation commutes with reduct, that is, given $\Sigma_1 \leq \Sigma_2$ in $\mathcal{I}_1$ and a $\Phi(\Sigma_2)$-model $M$ in $\mathcal{I}_2$,

$$ \beta_{\Sigma_2}(M)|_{\Sigma_1} = \beta_{\Sigma_1}(M|_{\Phi(\Sigma_1)}). $$

□
Some important properties of institution (co-)morphisms will be needed in the technical
development below:

**Definition 9 (Model-expansive, (weakly) exact, (weak) amalgamation).** An institute comorphism is **model-expansive**, if each $\beta_{\Sigma}$ is surjective. It is easy to show that model-expansive comorphisms faithfully encode logical consequence, that is, $\Gamma \models \varphi$ iff $\alpha(\Gamma) \models \alpha(\varphi)$.

An institute comorphism $\rho = (\Phi, \alpha, \beta) : \mathcal{I}_1 \to \mathcal{I}_2$ is **(weakly) exact**, if for each signature extension $\Sigma_1 \le \Sigma_2$ the diagram

<figure><img src="image_3.png" /></figure>

admits (weak) amalgamation, i.e. for any $M_2 \in \mathbf{Mod}^I(\Sigma_2)$ and $M'_1 \in \mathbf{Mod}^J(\Phi(\Sigma_1))$ with $M_2|_{\Sigma_1} = \beta_{\Sigma_1}(M'_1)$, there is a (not necessarily unique) $M'_2 \in \mathbf{Mod}^J(\Phi(\Sigma_2))$ with $\beta_{\Sigma_2}(M'_2) = M_2$ and $M'_2|_{\Phi(\Sigma_1)} = M'_1$. $\square$

Given these definitions, a **simple theoroidal institute comorphism** $\rho: \mathcal{I}_1 \to \mathcal{I}_2$ is an ordinary institute comorphism $\rho: \mathcal{I}_1 \to \mathcal{I}_2^{th}$ (for $\mathcal{I}_2^{th}$, see Def. 4). Moreover, an institute comorphism is said to be **model-isomorphic** if $\beta_{\Sigma}$ is an isomorphism. It is a **subinstitute comorphism** (cf. also [25]), if moreover the signature translation is an embedding and sentence translation is injective. The intuition is that theories should be embedded, while models should be represented exactly (such that model-theoretic results carry over).

# 4 A DOL Kernel and Its Semantics

The Distributed Ontology Language (DOL) shares many features with the language HetCASL [26] which underlies the Heterogeneous Tool Set Hets [29]. However, it also adds a number of new features:

- minimisation of models following the circumscription paradigm [24, 19];

- ontology module extraction, i.e. the extraction of a subtheory that contains all relevant logical information w.r.t. some subsignature [14];

- projections of theories to a sublogic;

- ontology alignments, which involve partial or even relational variants of signature morphisms [6];

- combination of theories via colimits, which has been used to formalise certain forms of ontology alignment [37, 17];

- referencing of all items by URLs, or, more general, IRIs [18].
Sannella and Tarlecki [32, 33] show that the structuring of logical theories (specifications) can be defined independently of the underlying logical system. They define a kernel language for structured specification that can be interpreted over an arbitrary institution.

Similar to [32] and also integrating heterogeneous constructs from [36, 30], we now introduce a kernel language for heterogeneous structured specifications for DOL. We will use the term “structured ontology” instead of “structured specification” to stress the intended use for DOL.

Since DOL involves not only one, but possibly several ontology languages, we need to introduce the notion of a 'heterogeneous logical environment'.

**Definition 10 (Heterogeneous logical environment).** A heterogeneous logical environment is defined to be a graph of institutes and institute morphisms and (possibly simple theoroidal) comorphisms, where we assume that some of the comorphisms (including all obvious identity comorphisms) are marked as default inclusions. The default inclusions are assumed to form a partial order on the institutes of the logic graph. If $\mathcal{I}_1 \subseteq \mathcal{I}_2$, the default inclusion is denoted by $\iota: \mathcal{I}_1 \to \mathcal{I}_2$. For any pair of institutes $\mathcal{I}_1$ and $\mathcal{I}_2$, if their supremum exists, we denote it by $\mathcal{I}_1 \cup \mathcal{I}_2$, and the corresponding default inclusions by $\iota_i: \mathcal{I}_i \to \mathcal{I}_1 \cup \mathcal{I}_2$.

We are now ready for the definition of heterogeneous structured ontology.

**Definition 11 (Heterogeneous structured ontology - DOL kernel language).** Let a heterogeneous logical environment be given. We inductively define the notion of heterogeneous structured ontology (in the sequel: ontology). Simultaneously, we define functions **Ins**, **Sig** and **Mod** yielding the institute, the signature and the model class of such an ontology.

**presentations:** For any institute $\mathcal{I}$, signature $\Sigma \in |\text{Sign}^\mathcal{I}|$ and finite set $\Gamma \subseteq \text{Sen}^\mathcal{I}(\Sigma)$ of $\Sigma$-sentences, the presentation $\langle \mathcal{I}, \Sigma, \Gamma \rangle$ is an ontology with:

$$ \text{Ins}(\langle \mathcal{I}, \Sigma, \Gamma \rangle) := \mathcal{I} $$

$$ \text{Sig}(\langle \mathcal{I}, \Sigma, \Gamma \rangle) := \Sigma $$

$$ \text{Mod}(\langle \mathcal{I}, \Sigma, \Gamma \rangle) := \{ M \in \text{Mod}(\Sigma) \mid M \models \Gamma \} $$

**union:** For any signature $\Sigma \in |\text{Sign}|$, given ontologies $O_1$ and $O_2$ with the same institute $\mathcal{I}$ and signature $\Sigma$, their union $O_1$ and $O_2$ is an ontology with:

$$ \text{Ins}(O_1 \text{ and } O_2) := \mathcal{I} $$

$$ \text{Sig}(O_1 \text{ and } O_2) := \Sigma $$

$$ \text{Mod}(O_1 \text{ and } O_2) := \text{Mod}(O_1) \cap \text{Mod}(O_2) $$

**extension:** For any ontology $O$ with institute $\mathcal{I}$ and signature $\Sigma$ and any signature extension $\Sigma \subseteq \Sigma'$ in $\mathcal{I}$, $O$ with $\Sigma'$ is an ontology with:

$$ \text{Ins}(O \text{ with } \Sigma') := \mathcal{I} $$

$$ \text{Sig}(O \text{ with } \Sigma') := \Sigma' $$

$$ \text{Mod}(O \text{ with } \Sigma') := \{ M' \in \text{Mod}(\Sigma') \mid M' \models \Sigma \} $$

**hiding:** For any ontology $O'$ with institute $\mathcal{I}$ and signature $\Sigma'$ and any signature extension $\Sigma \subseteq \Sigma'$ in $\mathcal{I}$, $O'$ hide $\Sigma$ is an ontology with:
$$ \mathbf{Ins}(O' \ hide \ \Sigma) := \mathcal{I} $$

$$ \mathbf{Sig}(O' \ hide \ \Sigma) := \Sigma $$

$$ \mathbf{Mod}(O' \ hide \ \Sigma) := \{M'|_{\Sigma} | M' \in \mathbf{Mod}(O')\} $$

**minimisation:** Let O be an ontology with institute $\mathcal{I}$ and signature $\Sigma$ and let $\Sigma_{min}$, $\Sigma_{fixed}$ be subsignatures of $\Sigma$ such that $\Sigma_{min} \cup \Sigma_{fixed}$ is defined. Intuitively, the interpretation of the symbols in $\Sigma_{min}$ will be minimised among those models interpreting the symbols in $\Sigma_{fixed}$ in the same way, while the interpretation of all symbols outside $\Sigma_{min} \cup \Sigma_{fixed}$ may vary arbitrarily. Then O **minimize** $\Sigma_{min}$, $\Sigma_{fixed}$ is an ontology with:

$$ \mathbf{Ins}(O \ minimize \ \Sigma_{min}, \Sigma_{fixed}) := \mathcal{I} $$

$$ \mathbf{Sig}(O \ minimize \ \Sigma_{min}, \Sigma_{fixed}) := \Sigma $$

$$ \mathbf{Mod}(O \ minimize \ \Sigma_{min}, \Sigma_{fixed}) := \{M \in \mathbf{Mod}(O) | M|_{\Sigma_{min} \cup \Sigma_{fixed}} \text{ is minimal in } \mathrm{Fix}(M)\} \\ \text{where } \mathrm{Fix}(M) = \{M' \in \mathbf{Mod}(O) | \Sigma_{min} \cup \Sigma_{fixed} | M'|_{\Sigma_{fixed}} = M|_{\Sigma_{fixed}}\} $$

**translation along a comorphism:** For any ontology O with institute $\mathcal{I}$ and signature $\Sigma$ and any institute comorphism $\rho = (\Phi, \alpha, \beta): \mathcal{I} \to \mathcal{I}', O \ with \ \rho$ is an ontology with:

$$ \mathbf{Ins}(O \ with \ \rho) := \mathcal{I}' $$

$$ \mathbf{Sig}(O \ with \ \rho) := \Phi(\Sigma) $$

$$ \mathbf{Mod}(O \ with \ \rho) := \{M' \in \mathbf{Mod}^{\mathcal{I}'}(\Phi(\Sigma)) | \beta_{\Sigma}(M') \in \mathbf{Mod}(O)\} $$

If $\rho$ is simple theoroidal, then $\mathbf{Sig}(O \ with \ \rho)$ is the signature component of $\Phi(\Sigma)$.

**hiding along a morphism:** For any ontology $O'$ with institute $\mathcal{I}$ and signature $\Sigma'$ and any institute morphism $\mu = (\Phi, \alpha, \beta): \mathcal{I} \to \mathcal{I}', O' \ hide \ \mu$ is an ontology with:

$$ \mathbf{Ins}(O' \ hide \ \mu) := \mathcal{I}' $$

$$ \mathbf{Sig}(O' \ hide \ \mu) := \Phi(\Sigma) $$

$$ \mathbf{Mod}(O' \ hide \ \mu) := \{\beta_{\Sigma}(M') | M' \in \mathbf{Mod}(O')\} $$

□

*Derived operations.* We also define the following derived operation generalising union to arbitrary pairs of ontologies: For any ontologies $O_1$ and $O_2$ with institutes $\mathcal{I}_1$ and $\mathcal{I}_2$ and signatures $\Sigma_1$ and $\Sigma_2$, if the supremum $\mathcal{I}_1 \cup \mathcal{I}_2$ exists and the union $\Sigma = \Phi(\Sigma_1) \cup \Phi(\Sigma_2)$ is defined, the *generalised union* of $O_1$ and $O_2$, by abuse of notation also written as $O_1$ **and** $O_2$, is defined as

$$ (O_1 \ with \ \iota_1 \ with \ \Sigma) \text{ and } (O_2 \ with \ \iota_2 \ with \ \Sigma) $$

The full DOL language adds further language constructs that can be expressed in terms of this kernel language. Furthermore, DOL allows the omission of translations along default inclusion comorphisms, since these can be reconstructed in a unique way.

*Logical consequence.* We say that a sentence $\varphi$ is a logical consequence of a heterogeneous structured ontology O, written $O \models \varphi$, if any model of O satisfies $\varphi$.

*Monotonicity.* Similar to [33], Ex. 5.1.4, we get:

**Proposition 12.** All structuring operations of the DOL kernel language except minimisation are monotone in the sense that they preserve model class inclusion: $\mathbf{Mod}(O_1) \subseteq \mathbf{Mod}(O_2)$ implies $\mathbf{Mod}(\mathrm{op}(O_1)) \subseteq \mathbf{Mod}(\mathrm{op}(O_2))$. (Union is monotone in both arguments.)
Indeed, the minimisation is a deliberate exception: its motivation is to capture non-monotonic reasoning.

**Proposition 13.** If reducts are surjective, **minimize** is anti-monotone in $\Sigma_{min}$.

*Proof.* Let $O$ be an ontology with institute $\mathcal{I}$ and signature $\Sigma$ and let $\Sigma_{min}^1, \Sigma_{min}^2, \Sigma_{fixed} \subseteq \Sigma$ be subsignatures such that $\Sigma_{min}^1 \le \Sigma_{min}^2$, and $\Sigma_{min}^i \cup \Sigma_{fixed}$ is defined for $i = 1, 2$. Let $Fix^1$ and $Fix^2$ defined as $Fix$ above, using $\Sigma_{min}^1$ and $\Sigma_{min}^2$ respectively. Let $M \in \mathbf{Mod}(O \text{ minimize } \Sigma_{min}^2, \Sigma_{fixed})$. Then $M$ is an $O$-model such that $M|_{\Sigma_{min}^2 \cup \Sigma_{fixed}}$ is minimal in $Fix^2(M)$. We show that $M|_{\Sigma_{min}^1 \cup \Sigma_{fixed}}$ is minimal in $Fix^1(M)$: Let $M'$ be in $Fix^1(M)$. By surjectivity of reducts, it can be expanded to a $\Sigma_{min}^2 \cup \Sigma_{fixed}$-model $M''$. Now $M'' \in Fix^2(M)$, because all involved models agree on $\Sigma_{fixed}$. Since $M|_{\Sigma_{min}^2 \cup \Sigma_{fixed}}$ is minimal in $Fix^2(M)$, $M|_{\Sigma_{min}^2 \cup \Sigma_{fixed}} \le M''$. Since reducts preserve the model ordering, $M|_{\Sigma_{min}^1 \cup \Sigma_{fixed}} \le M'$. Hence, $M \in \mathbf{Mod}(O \text{ minimize } \Sigma_{min}^1, \Sigma_{fixed})$. $\square$

# 5 Relations between Ontologies

Besides heterogeneous structured ontologies, DOL features the following statements about relations between heterogeneous structured ontologies:

**interpretations** Given heterogeneous structured ontologies $O_1$ and $O_2$ with institutes $\mathcal{I}_1$ and $\mathcal{I}_2$ and signatures $\Sigma_1$ and $\Sigma_2$, we write

$$O_1 \rightsquigarrow O_2$$

(read: $O_1$ can be interpreted in $O_2$) for the conjunction of

1. $\mathcal{I}_1 \subseteq \mathcal{I}_2$ with default inclusion $\iota = (\Phi, \alpha, \beta) : \mathcal{I}_1 \to \mathcal{I}_2$,

2. $\Phi(\Sigma_1) \le \Sigma_2$, and

3. $\beta(\mathbf{Mod}(O_2)|_{\Phi(\Sigma_1)}) \subseteq \mathbf{Mod}(O_1)$.

**modules** Given heterogeneous structured ontologies $O_1$ and $O_2$ over the same institute $\mathcal{I}$ with signatures $\Sigma_1$ and $\Sigma_2$, and given another signature $\Sigma \le \Sigma_1$ (called the restriction signature), we say that

$O_1$ is a model-theoretic (consequence-theoretic) module of $O_2$ w.r.t. $\Sigma$

if for any $O_1$-model $M_1$, $M_1|_{\Sigma}$ can be extended to an $O_2$-model (resp. $O_2$ is a conservative extension of $O_1$, see Def. 5). It is easy to see that the model-theoretic module relation implies the consequence-theoretic one. However, the converse is not true in general, compare [20] for an example from description logic, and see [15] for more general conservativity preservation results.

We first considered to integrate a module extraction operator into the kernel language of heterogeneous structured ontologies. However, there are so many different notions of ontology module and techniques of module extraction used in the literature that we would have to define a whole collection of module extraction operators, a collection that moreover would quickly become obsolete and incomplete. We refrained from this,
and instead provide a relation between heterogeneous structured ontologies that is in-
dependent of the specificities of particular module extraction operators.

Still, it is possible to define all the relevant notions used in the ontology modules
community within an arbitrary institute, namely the notions of conservative extension,
inseparability, uniform interpolant etc. The reason is that these notions typically are
defined in set-theoretic parlance about signatures (see Def. 5).

The full DOL language is based on the DOL kernel and also includes a construct for colimits (which is omitted here, because its semantics requires institutions) and ontology alignments (which are omitted here, because they do not have a model-theoretic semantics). The full DOL language is detailed in the current OntoIOp ISO 17347 working draft, see ontoiop.org. There, also an alternative semantics to the above direct set-theoretic semantics is given: a translational semantics. It assumes that all involved institutes can be translated to Common Logic, and gives the semantics of an arbitrary ontology by translation to Common Logic (and then using the above direct semantics). The two semantics are compatible, see [28] for details. However, the translational semantics has some important drawbacks. In particular, the semantics of ontology modules (relying on the notion of conservative extension) is not always preserved when translating to Common Logic. See [28] for details.

6 An Example in DOL

As an example of a heterogeneous ontology in DOL, we formalise some notions of
mereology. Propositional logic is not capable of describing mereological *relations*, but
of describing the basic categories over which the DOLCE foundational ontology [23]
defines mereological relations. The same knowledge can be formalised more conve-
niently in OWL, which additionally allows for describing (not defining!) basic part-
hood properties. As our OWL ontology redeclares as classes the same categories that
the propositional logic ontology *Taxonomy* had introduced as propositional variables,
using different names but satisfying the same disjointness and subsumption axioms,
we observe that it *interprets* the former. Mereological relations are frequently *used* in
lightweight OWL ontologies, e.g. biomedical ontologies in the EL profile (designed for
efficient reasoning with a large number of entities, a frequent case in this domain), but
these languages are not fully capable of *defining* these relations. Therefore, we finally
provide a full definition of several mereological relations in first order logic, in the Com-
mon Logic language, by importing, translating and extending the OWL ontology. We
use Common Logic's second-order facility of quantifying over predicates to concisely
express the restriction of the variables *x*, *y*, and *z* to the same taxonomic category.

%prefix( :
<http://www.example.org/mereology#>
owl: <http://www.w3.org/2002/07/owl#>
log: <http://purl.net/dol/logics/>
trans: <http://purl.net/dol/translations/>
ser: <http://purl.net/dol/serializations/>)

% prefix for this distributed ontology
%% OWL basic ontology language
%% DOL-conforming logics (Fig. 1)
%% translations between these logics
%% serializations, i.e. concrete syntaxes

distributed-ontology Mereology

logic log:Propositional syntax ser:Prop/Hets % non-standard serialization built into Hets

ontology Taxonomy = % basic taxonomic information about mereology reused from DOLCE

props PT, T, S, AR, PD

. S ∨ T ∨ AR ∨ PD —→ PT

% PT is the top concept
. S ∧ T → ⊥

. T ∧ AR → ⊥

% PD, S, T, AR are pairwise disjoint

% and so on

logic log:SROIQ syntax ser:OWL2/Manchester

% OWL Manchester syntax

ontology BasicParthood =

% Parthood in SROIQ, as far as expressible

Class: ParticularCategory SubClassOf: Particular % omitted similar declarations of the other classes

DisjointUnionOf: SpaceRegion, TimeInterval, AbstractRegion, Perdurant

% pairwise disjointness more compact thanks to an OWL built-in

ObjectProperty: isPartOf Characteristics: Transitive

ObjectProperty: isProperPartOf Characteristics: Asymmetric SubPropertyOf: isPartOf

Class: Atom EquivalentTo: inverse isProperPartOf only owl:Nothing

interpretation TaxonomyToParthood : Taxonomy to BasicParthood =

translate with trans:PropositionalToSROIQ, % translate the logic, then rename the entities

PT ↦ Particular, S ↦ SpaceRegion, T ↦ TimeInterval, A ↦ AbstractRegion, %[ and so on ]%

logic log:CommonLogic syntax ser:CommonLogic/CLIF % syntax: the Lisp-like CLIF dialect of Common Logic

ontology ClassicalExtensionalParthood =

BasicParthood translate with trans:SROIQtoCL % import the OWL ontology from above, translate it ...

then { % ... to Common Logic, then extend it there:

(forall (X) (if (or (= X S) (= X T) (= X AR) (= X PD))

(forall (x y z) (if (and (X x) (X y) (X z))

(and % now list all the axioms

(if (and (isPartOf x y) (isPartOf y x)) (= x y)) % antisymmetry

(if (and (isProperPartOf x y) (isProperPartOf y z)) (isProperPartOf x z))

% transitivity; can't be expressed in OWL together with asymmetry

(iff (overlaps x y) (exists (pt) (and (isPartOf pt x) (isPartOf pt y))))

(iff (isAtomicPartOf x y) (and (isPartOf x y) (Atom x)))

(iff (sum z x y) (forall (w) (iff (overlaps w z) (and (overlaps w x) (overlaps w y)))))

(exists (s) (sum s x y)))))) % existence of the sum

}

# 7 Relating Institutes and institutions

In this section, we show that institutes are a certain restriction of institutions. We first recall Goguen's and Burstall's notion of institution [10], which they have introduced as a formalisation of the intuitive notion of logical system. We assume some acquaintance with the basic notions of category theory and refer to [1] or [22] for an introduction.

**Definition 14.** An institution is a quadruple $I = (\mathbf{Sign}, \mathbf{Sen}, \mathbf{Mod}, |=$) consisting of the following:

- a category **Sign** of signatures and signature morphisms,

- a functor **Sen**: **Sign** $\to$ **Set**<fnref n="8" /> giving, for each signature $\Sigma$, the set of sentences **Sen**($\Sigma$), and for each signature morphism $\sigma$: $\Sigma \to \Sigma'$, the sentence translation map **Sen**($\sigma$): **Sen**($\Sigma$) $\to$ **Sen**($\Sigma'$), where often **Sen**($\sigma$)(φ) is written as $\sigma(\varphi)$,

- a functor **Mod**: **Sign**$^{op}$ $\to$ **CAT**<fnref n="9" /> giving, for each signature $\Sigma$, the category of models **Mod**($\Sigma$), and for each signature morphism $\sigma$: $\Sigma \to \Sigma'$, the reduct functor **Mod**($\sigma$): **Mod**($\Sigma'$) $\to$ **Mod**($\Sigma$), where often **Mod**($\sigma$)(M') is written as $M'|_{\sigma}$, and $M'|_{\sigma}$ is called the $\sigma$-reduct of M', while M' is called a $\sigma$-expansion of M'|$_{\sigma}$,

- a satisfaction relation $|\Sigma = \subseteq$ $|\mathbf{Mod}(\Sigma)| \times \mathbf{Sen}(\Sigma)$ for each $\Sigma \in |\mathbf{Sign}|$,

<footnote n="8">⁸ **Set** is the category having all small sets as objects and functions as arrows.</footnote>

<footnote n="9">⁹ **CAT** is the category of categories and functors. Strictly speaking, **CAT** is not a category but only a so-called quasicategory, which is a category that lives in a higher set-theoretic universe.</footnote>
such that for each $\sigma: \Sigma \to \Sigma'$ in **Sign** the following satisfaction condition holds:

$$ (\star) \quad M' \models_{\Sigma'} \sigma(\varphi) \text{ iff } M'|_{\sigma} \models_{\Sigma} \varphi $$

for each $M' \in \mathbf{Mod}(\Sigma')$ and $\varphi \in \mathbf{Sen}(\Sigma)$, expressing that truth is invariant under change of notation and context.<fnref n="10" /> □

With institutions, a few more features of DOL can be equipped with a semantics:

- renamings along signature morphisms [32],

- combinations (colimits), and

- monomorphic extensions.

Due to the central role of inclusions of signatures for institutes, we also need to recall the notion of inclusive institution.

**Definition 15** ([31]). *An inclusive category is a category having a broad subcategory which is a partially ordered class.*

*An inclusive institution is one with an inclusive signature category such that the sentence functor preserves inclusions. We additionally require that such institutions*

- have inclusive model categories,

- have signature intersections (i.e. binary infima), which are preserved by **Sen**,<fnref n="11" /> and

- have well-founded sentences, which means that there is no sentence that occurs in all sets of an infinite chain of strict inclusions

$$ \dots \hookrightarrow \mathbf{Sen}(\Sigma_n) \hookrightarrow \dots \hookrightarrow \mathbf{Sen}(\Sigma_1) \hookrightarrow \mathbf{Sen}(\Sigma_o) $$

that is the image (under **Sen**) of a corresponding chain of signature inclusions. □

**Definition 16.** *Given institutions I and J, an institution morphism [10] written $\mu = (\Phi, \alpha, \beta): I \to J$ consists of*

- a functor $\Phi: \mathbf{Sign}^I \to \mathbf{Sign}^J$,

- a natural transformation $\alpha: \mathbf{Sen}^I \circ \Phi \to \mathbf{Sen}^J$ and

- a natural transformation $\beta: \mathbf{Mod}^I \to \mathbf{Mod}^J \circ \Phi^{op}$,

such that the following satisfaction condition holds for all $\Sigma \in \mathbf{Sign}^I$, $M \in \mathbf{Mod}^I(\Sigma)$ and $\varphi' \in \mathbf{Sen}^J(\Phi(\Sigma)):

$$ M \models_{\Sigma}^{I} \alpha_{\Sigma}(\varphi') \text{ iff } \beta_{\Sigma}(M) \models_{\Phi(\Sigma)}^{J} \varphi' $$

**Definition 17.** *Given institutions I and J, an institution comorphism [9] denoted as $\rho = (\Phi, \alpha, \beta): I \to J$ consists of*

<footnote n="10">¹⁰ Note, however, that non-monotonic formalisms can only indirectly be covered this way, but compare, e.g., [12].</footnote>

<footnote n="11">¹¹ This is a quite reasonable assumption met by practically all institutions. Note that by contrast, preservation of unions is quite unrealistic—the union of signatures normally leads to new sentences combining symbols from both signatures.</footnote>
- a functor $\Phi: \text{Sign}^I \to \text{Sign}^J$,

- a natural transformation $\alpha: \text{Sen}^I \to \text{Sen}^J \circ \Phi$,

- a natural transformation $\beta: \text{Mod}^J \circ \Phi^{op} \to \text{Mod}^I$

such that the following satisfaction condition holds for all $\Sigma \in \text{Sign}^I$, $M' \in \text{Mod}^J(\Phi(\Sigma))$ and $\varphi \in \text{Sen}^I(\Sigma)$:

$$M' \models_{\Phi(\Sigma)}^{J} \alpha_{\Sigma}(\varphi) \text{ iff } \beta_{\Sigma}(M') \models_{\Sigma}^{I} \varphi.$$

Let **InclIns** (**CoInclIns**) denote the quasicategory of inclusive institutions and morphisms (comorphisms). Furthermore, let **Class** denote the quasicategory of classes and functions. Note that (class-indexed) colimits of sets in **Class** can be constructed in the same way as in **Set**. Finally, call an institute **locally small**, if each **Sen**(Σ) is a set. Let **Institute** (**CoInstitute**) be the quasicategory of locally small institutes and morphisms (comorphisms).

**Proposition 18.** *There are functors $F^{co}: \text{CoInstitute} \to \text{CoInclIns}$ and $F: \text{Institute} \to \text{InclIns}$.*

*Proof.* Given an institute $\mathcal{I} = (\text{Sen}^{\mathcal{I}}, \text{Sign}^{\mathcal{I}}, \leq^{\mathcal{I}}, \text{sig}^{\mathcal{I}}, \text{Mod}^{\mathcal{I}}, \models^{\mathcal{I}}, \perp|.)$, we construct an institution $F(\mathcal{I}) = F^{co}(\mathcal{I})$ as follows: $(\text{Sign}^{\mathcal{I}}, \leq^{\mathcal{I}})$ is a partially ordered class, hence a (thin) category. We turn it into an inclusive category by letting all morphisms be inclusions. This will be the signature category of $F(\mathcal{I})$.

For each signature $\Sigma$, we let $\text{Sen}^{F(\mathcal{I})}(\Sigma)$ be $\text{Sen}^{\mathcal{I}}(\Sigma)$ (here we need local smallness of $\mathcal{I}$). Then $\text{Sen}^{F(\mathcal{I})}$ easily turns into an inclusion-preserving functor. Also, $\text{Mod}^{F(\mathcal{I})}(\Sigma)$ is $\text{Mod}^{\mathcal{I}}(\Sigma)$ turned into a thin category using the partial order on $\text{Mod}^{\mathcal{I}}$. Since reducts are compositional and preserve the model ordering, we obtain reduct functors for $F(\mathcal{I})$. Satisfaction in $F(\mathcal{I})$ is defined as in $\mathcal{I}$. The satisfaction condition holds because satisfaction is invariant under reduct.

Given an institute comorphism $\rho = (\Phi, \alpha, \beta): \mathcal{I}_1 \to \mathcal{I}_2$, we define an institution comorphism $F^{co}(\rho): F(\mathcal{I}_1) \to F(\mathcal{I}_2)$ as follows. $\Phi$ obviously is a functor from $\text{Sign}^{F(\mathcal{I}_1)}$ to $\text{Sign}^{F(\mathcal{I}_2)}$. If $\text{sig}(\varphi) \leq \Sigma$, by sentence coherence, $\text{sig}(\alpha(\varphi)) \leq \Phi(\Sigma)$. Hence, $\alpha: \text{Sen}_1 \to \text{Sen}_2$ can be restricted to $\alpha_{\Sigma}: \text{Sen}_1(\Sigma) \to \text{Sen}_2(\Sigma)$ for any $\mathcal{I}_1$-signature $\Sigma$. Naturality of the family $(\alpha_{\Sigma})_{\Sigma \in \text{Sign}_1}$ follows from the fact that the $\alpha_{\Sigma}$ are restrictions of a global $\alpha$. Each $\beta_{\Sigma}$ is functorial because it is monotone. Naturality of the family $(\beta_{\Sigma})_{\Sigma \in \text{Sign}_1}$ follows from model translation commuting with reduct. The satisfaction condition is easily inherited from the institute comorphism.

The translation of institute morphisms is similar. □

**Proposition 19.** *There are functors $G^{co}: \text{CoInclIns} \to \text{CoInstitute}$ and $G: \text{InclIns} \to \text{Institute}$, such that $G^{co} \circ F^{co} \cong \text{id}$ and $G \circ F \cong \text{id}$.*

*Proof.* Given an inclusive institution $\mathcal{I} = (\text{Sign}^{\mathcal{I}}, \text{Sen}^{\mathcal{I}}, \text{Mod}^{\mathcal{I}}, \models^{\mathcal{I}})$, we construct an institute $G(\mathcal{I}) = G^{co}(\mathcal{I})$ as follows: $(\text{Sign}^{\mathcal{I}}, \leq^{\mathcal{I}})$ is the partial order given by the inclusions.

$\text{Sen}^{G(\mathcal{I})}$ is the colimit of the diagram of all inclusions $\text{Sen}^{\mathcal{I}}(\Sigma_1) \hookrightarrow \text{Sen}^{\mathcal{I}}(\Sigma_1)$ for $\Sigma_1 \leq \Sigma_2$. This colimit is taken in the quasicategory of classes and functions. It exists because all involved objects are sets (the construction can be given as a quotient of the
disjoint union, following the usual construction of colimits as coequalisers of coproducts). Let $\mu_{\Sigma} : \mathbf{Sen}^{\mathcal{I}}(\Sigma) \to \mathbf{Sen}^{G(\mathcal{I})}$ denote the colimit injections. For a sentence $\varphi$, let $S(\varphi)$ be the set of signatures $\Sigma$ such that $\varphi$ is in the image of $\mu_{\Sigma}$. We show that $S(\varphi)$ has a least element. For if not, choose some $\Sigma_0 \in S(\varphi)$. Assume that we have chosen $\Sigma_n \in S(\varphi)$. Since $\Sigma_n$ is not the least element of $S(\varphi)$, there must be some $\Sigma \in S(\varphi)$ such that $\Sigma_n \not\le \Sigma$. Then let $\Sigma_{n+1} = \Sigma_n \cap \Sigma$; since Sen preserves intersections, $\Sigma_{n+1} \in S(\varphi)$. Moreover, $\Sigma_{n+1} < \Sigma_n$. This gives an infinite descending chain of signature inclusions in $S(\varphi)$, contradicting $\mathcal{I}$ having well-founded sentences. Hence, $S(\varphi)$ must have a least element, which we use as $\mathrm{sig}(\varphi)$.

$\mathbf{Mod}^{G(\mathcal{I})}(\Sigma)$ is the partial order of inclusions in $\mathbf{Mod}^{\mathcal{I}}(\Sigma)$, and also reduct is inherited. Since $\mathbf{Mod}^{G(\mathcal{I})}$ is functorial, reducts are compositional. Since each $\mathbf{Mod}^{G(\mathcal{I})}(\sigma)$ is functorial, reducts preserve the model ordering. Satisfaction in $G(\mathcal{I})$ is defined as in $\mathcal{I}$. The satisfaction condition implies that satisfaction is invariant under reduct.

Given an institution comorphism $\rho = (\Phi, \alpha, \beta) : \mathcal{I}_1 \to \mathcal{I}_2$, we define an institute comorphism $G^{co}(\rho) : G(\mathcal{I}_1) \to G(\mathcal{I}_2)$ as follows. $\Phi$ obviously is a monotone map from $\mathbf{Sign}^{G(\mathcal{I}_1)}$ to $\mathbf{Sign}^{G(\mathcal{I}_2)}$.

$\alpha$: $\mathbf{Sen}^{G(\mathcal{I}_1)} \to \mathbf{Sen}^{G(\mathcal{I}_2)}$ is defined by exploiting the universal property of the colimit $\mathbf{Sen}^{G(\mathcal{I}_1)}$: it suffices to define a cocone $\mathbf{Sen}^{\mathcal{I}_1}(\Sigma) \to \mathbf{Sen}^{G(\mathcal{I}_2)}$ indexed over signatures $\Sigma$ in $\mathbf{Sign}^{\mathcal{I}_1}$. The cocone is given by composing $\alpha_{\Sigma}$ with the inclusion of $\mathbf{Sen}^{\mathcal{I}_1}(\Phi(\Sigma))$ into $\mathbf{Sen}^{G(\mathcal{I}_2)}$. Commutativity of a cocone triangle follows from that of a cocone triangle for the colimit $\mathbf{Sen}^{G(\mathcal{I}_2)}$ together with naturality of $\alpha$. This construction also ensures sentence coherence.

Model translation is just given by the $\beta_{\Sigma}$; the translation of institution morphisms is similar.

Finally, $G \circ F \cong \mathrm{id}$ follows because $\mathbf{Sen}$ can be seen to be the colimit of all $\mathbf{Sen}(\Sigma_1) \hookrightarrow \mathbf{Sen}(\Sigma_2)$. This means that we can even obtain $G \circ F = \mathrm{id}$. However, since the choice of the colimit in the definition of $G$ is only up to isomorphism, generally we obtain only $G \circ F \cong \mathrm{id}$. The argument for $G^{co} \circ F^{co} \cong \mathrm{id}$ is similar, since isomorphism institution morphisms are also isomorphism institution comorphisms. $\square$

It should be noted that $F^{co} : \mathbf{CoInstitute} \to \mathbf{CoInclIns}$ is “almost” left adjoint to $G^{co} : \mathbf{CoInclIns} \to \mathbf{CoInstitute}$. By the above remarks, w.l.o.g., the unit $\eta : \mathrm{Id} \to G^{co} \circ F^{co}$ can be chosen to be the identity. Hence, we need to show that for each institute comorphism $\rho : \mathcal{I}_1 \to G(\mathcal{I}_2)$, there is a unique institution comorphism $\rho^# : F(\mathcal{I}_1) \to \mathcal{I}_2$ with $G(\rho^#) = \rho$. The latter condition easily ensures uniqueness. Let $\rho = (\Phi, \alpha, \beta)$. We construct $\rho^#$ as $(\Phi, \alpha^#, \beta)$. Clearly, $\Phi$ also is a functor from $\mathbf{Sign}^{F(\mathcal{I}_1)}$ into $\mathbf{Sign}^{\mathcal{I}_2}$ (which is a supercategory of $\mathbf{Sign}^{G(\mathcal{I}_2)}$). A similar remark holds for $\beta$, but only if the model categories in $\mathcal{I}_2$ consist of inclusions only. $\alpha^#$ can be constructed from $\alpha$ by passing to the restrictions $\alpha_{\Sigma}$. Altogether we get:

**Proposition 20.** $F^{co} : \mathbf{CoInstitute} \to \mathbf{CoInclIns}$ is left adjoint to $G^{co} : \mathbf{CoInclIns} \to \mathbf{CoInstitute}$ if institutions are restricted to model categories in consisting of inclusions only.

Since also $G^{co} \circ F^{co} \cong \mathrm{id}$, **CoInstitute** comes close to being a coreflective subcategory of **CoInclIns**.
We also obtain:

**Proposition 21.** For the DOL kernel language, the institute-based semantics (over some institute-based heterogeneous logical environment $\mathcal{E}$) and the institution-based semantics (similar to that given in [32, 30], over $\mathcal{F}$ applied to $\mathcal{E}$) coincide up to application of $\mathcal{G}$ to the **Ins** component of the semantics.

## 8 Conclusion

We have taken concepts from the area of formal methods for software specification and applied them to obtain a kernel language for the Distributed Ontology Language (DOL), including a semantics, and have thus provided the syntax and semantics of a heterogeneous structuring language for ontologies. The standard approach here would be to use institutions to formalise the notion of logical system. However, aiming at a more simple presentation of the heterogeneous semantics, we here develop the notion of **institute** which allows us to obtain a set-based semantics for a large part of DOL. Institutes can be seen as institutions without category theory.

Goguen and Tracz [11] have a related set-theoretic approach to institutions: they require signatures to be tuple sets. Our approach is more abstract, because signatures can be any partial order. Moreover, the results of Sect. 7 show that institutes integrate nicely with institutions. That is, we can have the cake and eat it, too: we can abstractly formalise various logics as institutes, a formalisation which, being based on standard set-theoretic methods, can be easily understood by the broader ontology communities that are not necessarily acquainted with category theoretic methods. Moreover, the possibility to extend the institute-based formalisation to a full-blown institution which is compatible with the institute (technically, this means that the functor $\mathcal{G}$ defined in Prop. 19, applied to the institution, should yield the institute), allows a smooth technical integration of further features into the framework which do require institutions, such as colimits.

This work provides the semantic backbone for the Distributed Ontology Language DOL, which is being developed in the ISO Standard 17347 Ontology Integration and Interoperability, see ontoiop.org. An experimental repository for ontologies written in different logics and also in DOL is available at ontohub.org.

*Acknowledgements:* We would like to thank the OntoIOp working group within ISO/TC 37/SC 3 for providing valuable feedback, in particular Michael Grüninger, Pat Hayes, Maria Keet, Chris Menzel, and John Sowa. We also want to thank Andrzej Tarlecki, with whom we collaborate(d) on the semantics of heterogeneous specification, Thomas Schneider for help with the semantics of modules, and Christian Maeder, Eugen Kuksa and Sören Schulze for implementation work. This work has been supported by the DFG-funded Research Centre on Spatial Cognition (SFB/TR 8), project I1-[OntoSpace], and EPSRC grant "EP/J007498/1".
References

1. J. Adámek, H. Herrlich, and G. Strecker. *Abstract and Concrete Categories*. Wiley, New York, 1990.

2. A. Avron. Simple consequence relations. *Inf. Comput.*, 92(1):105–140, 1991.

3. E. Beisswanger, S. Schulz, H. Stenzhorn, and U. Hahn. BioTop: An upper domain ontology for the life sciences - a description of its current structure, contents, and interfaces to OBO ontologies. *Applied Ontology*, 3(4):205–212, 2008.

4. W.A. Carnielli, M. Coniglio, D.M. Gabbay, P. Gouveia, and C. Sernadas. *Analysis and synthesis of logics: how to cut and paste reasoning systems*. Applied logic series. Springer, 2008.

5. Common Logic Working Group. Common Logic: Abstract syntax and semantics. Technical report, 2003. http://iso-commonlogic.org.

6. Jérôme David, Jérôme Euzenat, François Scharffe, and Cássia Trojahn dos Santos. The alignment API 4.0. *Semantic Web*, 2(1):3–10, 2011.

7. R. Diaconescu. Grothendieck institutions. *Applied categorical structures*, 10:383–402, 2002.

8. G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, *The Collected Papers of Gerhard Gentzen*, pages 68–213. North-Holland, Amsterdam, 1969.

9. J. Goguen and G. Rosu. Institution morphisms. *Formal aspects of computing*, 13:274–307, 2002.

10. J. A. Goguen and R. M. Burstall. Institutions: Abstract model theory for specification and programming. *Journal of the Association for Computing Machinery*, 39:95–146, 1992. Predecessor in: LNCS 164, 221–256, 1984.

11. Joseph A. Goguen and Will Tracz. An implementation-oriented semantics for module composition. In Gary T. Leavens and Murali Sitaraman, editors, *Foundations of Component-Based Systems*, chapter 11, pages 231–263. Cambridge University Press, New York, NY, 2000.

12. Sofia Guerra. Composition of Default Specifications. *J. Log. Comput.*, 11(4):559–578, 2001.

13. Ian Horrocks, Oliver Kutz, and Ulrike Sattler. The Even More Irresistible SROIQ. In *Proc. of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR2006)*, pages 57–67. AAAI Press, June 2006.

14. Boris Konev, Carsten Lutz, Dirk Walther, and Frank Wolter. Formal properties of modularization. In H. Stuckenschmidt and S. Spaccapietra, editors, *Ontology Modularization*. Springer, 2008.

15. O. Kutz and T. Mossakowski. Conservativity in Structured Ontologies. In *18th European Conf. on Artificial Intelligence (ECAI-08)*, Patras, Greece, 2008. IOS Press.

16. O. Kutz, T. Mossakowski, and D. Lücke. Carnap, Goguen, and the Hyperontologies: Logical Pluralism and Heterogeneous Structuring in Ontology Design. *Logica Universalis*, 4(2):255–333, 2010. Special Issue on ‘Is Logic Universal?’.

17. O. Kutz, I. Normann, T. Mossakowski, and D. Walther. Chinese Whispers and Connected Alignments. In *Proc. of the 5th International Workshop on Ontology Matching (OM-2010)*, 9th International Semantic Web Conference ISWC-2010, November 7, 2010, Shanghai, China., 2010.

18. Christoph Lange, Till Mossakowski, and Oliver Kutz. LoLa: A Modular Ontology of Logics, Languages, and Translations. In Thomas Schneider and Dirk Walther, editors, *Modular Ontologies*, number 875 in CEUR Workshop Proceedings, Aachen, 2012.

19. V. Lifschitz. Circumscription. In *Handbook of Logic in Artificial Intelligence and Logic Programming*, volume 3, pages 297–352. Oxford University Press, 1994.

20. Carsten Lutz, Dirk Walther, and Frank Wolter. Conservative Extensions in Expressive Description Logics. In *Proceedings of IJCAI-07*, pages 453–458. AAAI Press, 2007.
21. Carsten Lutz and Frank Wolter. Deciding inseparability and conservative extensions in the description logic *EL*. *Journal of Symbolic Computation*, 45(2):194–228, 2010.

22. Saunders Mac Lane. *Categories for the Working Mathematician*. Springer, Berlin, 2nd edition, 1998.

23. Claudio Masolo, Stefano Borgo, Aldo Gangemi, Nicola Guarino, and Alessandro Oltramari. Ontology library. WonderWeb Deliverable 18, Laboratory for Applied Ontology – ISTC-CNR, December 2003.

24. John McCarthy. Circumscription - A Form of Non-Monotonic Reasoning. *Artif. Intell.*, 13(1-2):27–39, 1980.

25. J. Meseguer. General logics. In *Logic Colloquium 87*, pages 275–329. North Holland, 1989.

26. T. Mossakowski. *HetCASL* - Heterogeneous Specification. Language Summary, 2004. http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/HetCASL/HetCASL-Summary.pdf.

27. Till Mossakowski and Oliver Kutz. The Onto-Logical Translation Graph. In *Modular Ontologies—Proceedings of the Fifth International Workshop (WoMO 2011)*, volume 230 of *Frontiers in Artificial Intelligence and Applications*, pages 94–109. IOS Press, 2011.

28. Till Mossakowski, Christoph Lange, and Oliver Kutz. Three Semantics for the Core of the Distributed Ontology Language. In Maureen Donnelly and Giancarlo Guizzardi, editors, *FOIS 2012: 7th International Conference on Formal Ontology in Information Systems*, pages 337–352. IOS Press; Amsterdam; http://www.iospress.nl, 2012. Best paper award.

29. Till Mossakowski, Christian Maeder, and Klaus Lüttich. The Heterogeneous Tool Set. In Orna Grumberg and Michael Huth, editors, *TACAS 2007*, volume 4424 of *Lecture Notes in Computer Science*, pages 519–522. Springer-Verlag Heidelberg, 2007.

30. Till Mossakowski and Andrzej Tarlecki. Heterogeneous logical environments for distributed specifications. In Andrea Corradini and Ugo Montanari, editors, *WADT 2008*, volume 5486 of *Lecture Notes in Computer Science*, pages 266–289. Springer, 2009.

31. Grigore Roșu and Joseph Goguen. Composing hidden information modules over inclusive institutions. In Olaf Owe, Stein Krogdahl, and Tom Lyche, editors, *From Object-Orientation to Formal Methods. Essays in Memory of Ole-Johan Dahl*, volume 2635 of *Lecture Notes in Computer Science*, pages 96–123. Springer, 2004.

32. D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. *Information and Computation*, 76:165–210, 1988.

33. Donald Sannella and Andrzej Tarlecki. *Foundations of Algebraic Specification and Formal Software Development*. EATCS Monographs on theoretical computer science. Springer, 2012.

34. D. Scott. Rules and derived rules. In S. Stenlund, editor, *Logical Theory and Semantic Analysis*, pages 147–161. Reidel, 1974.

35. B. Smith, W. Ceusters, B. Klagges, J. Kohler, A. Kumar, J. Lomax, C.J. Mungall, F. Neuhaus, A. Rector, and C. Rosse. Relations in biomedical ontologies. *Genome Biology*, 6:R46, 2005.

36. A. Tarlecki. Towards heterogeneous specifications. In D. Gabbay and M. de Rijke, editors, *Frontiers of Combining Systems 2, 1998*, Studies in Logic and Computation, pages 337–360. Research Studies Press, 2000.

37. Antoine Zimmermann, Markus Krötzsch, J. Euzenat, and Pascal Hitzler. Formalizing Ontology Alignment and its Operations with Category Theory. In Brandon Bennett and Christiane Fellbaum, editors, *Proceedings of the Fourth International Conference on Formal Ontology in Information Systems (FOIS 2006)*, volume 150 of *Frontiers in Artificial Intelligence and Applications*, pages 277–288. IOS Press, NOV 2006.