In this paper, we show how the web ontology language OWL can be accommodated within the larger framework of the heterogeneous common algebraic specification language HETCASL. Through this change in perspective, OWL can benefit from various useful HETCASL features concerning structuring, modularity, and heterogeneity. This tackles a major problem area in ontology engineering: re-use of ontologies and re-combination of ontological modules. We discuss in particular: (1) the extension of the Manchester syntax for OWL with structuring mechanisms of CASL, allowing for explicit modularisation; (2) automatic translations between ontology languages to support ontology design across different ontology languages (heterogeneity); (3) heterogeneous ontology refinements, and corresponding automated reasoning support for different logics.
Ontologies play an increasingly important role in various areas of Knowledge Representation, ranging from the life sciences and engineering domains to linguistic semantics. In the process, ontologies are being designed in a broad spectrum of logics, with considerably varying expressivity and supporting quite different reasoning methods.
Many (domain) ontologies are written in description logics like S HOIN (D) (underlying OWL-DL) and S ROIQ(D) (underlying OWL 2.0). These logics are characterised by having a rather fine-tuned expressivity, exhibiting (still) decidable satisfiability problems, whilst being amenable to highly optimised implementations.
However, there are many cases where either weaker DLs are enough, such as
subBoolean E L, and more specialised (and faster) algorithms can be employed, or, contrarily,
the expressivity has to be extended beyond the scope of standard description logics. An
example for the former would be the NCI thesaurus (containing about 45.000 concepts)
which is intended to become the reference terminology for cancer research [
While the web ontology language OWL is being constantly refined and extended, its main target application is the Semantic Web and related areas, and it can thus not be expected to be fit for any purpose: there will always be new, typically interdisciplinary application areas for ontologies where the employed (or required) formal languages do not directly fit into the OWL landscape. Heterogeneity (of ontology languages) is thus clearly an important issue. This does not only include cases where the expressivity of OWL is simply exceeded (such as when moving to full first-order logic), but, ultimately, also cases where combinations with or connections to formalism with different semantics have to be covered, such as temporal, spatial, or epistemic logics, cf. e.g. [1; 2; 24; 10; 5].
In this context, it can be a rather difficult task for an ontology designer to choose an
appropriate logic and formalism for a specific ontology design beforehand—and failing
in making the right choice might lead to the necessity of re-designing large parts of an
ontology from scratch, or limit future expandability. Another issue is the mere size of
ontologies making the design process potentially quite hard and error prone (at least for
humans). This issue has been partly cured in OWL by the imports construct, but still
leaves the problem of ‘debugging’ large ontologies as an important issue [
We here propose a cure to the above issues based on the concept of heterogeneity: facing the fact that several logics and formalisms are used for designing ontologies, we suggest heterogeneous structuring constructs that allow to combine ontologies in various ways and in a systematic and formally and semantically well-founded way. Our approach is based on the theory of institutions and formal structuring techniques from algebraic specification theory (discussed in Sec. 2). Its main features are the following: – The ontology designer can use description logics to specify most parts of an ontology, and can use first-order (or even higher-order) logic where needed. Moreover, the overall ontology can be assembled from (and can be split up into) semantically meaningful parts (‘modules’) that are systematically related by structuring mechanisms.
These parts can then be re-used and/or extended in different settings. – Institution theory provides ‘logic translations’ between different ontology languages, translating the syntax and semantics of different formalisms. – Various concepts of ‘ontological module’ are covered, including simple imports (extensions) and union of theories, as well as conservative and definitional extensions. – Structuring into modules is made explicit in the ontology and generates so-called proof obligations for conservativity. Proof obligations can also be used to keep track of desired consequences of an ontology (module), especially during the design process. – Re-using (parts of) ontologies whilst renaming (parts of) the signature is handled by symbol maps and hiding symbols: essentially, this allows the internalisation of (strict) alignment mappings. – The approach allows heterogeneous refinements: it is possible to prove that an ontology O2 is a refinement of another ontology O1, formalised in a different logic. For instance, one can check if a domain ontology is a refinement of (a part of) a foundational one. An interesting by-product of the definition of heterogeneous refinements is that it also provides a rather general definition of heterogeneous sub-ontology.
We have formalised several logics that are important from an ontology-design
perspective as so-called institutions [
Tool support for developing heterogeneous ontologies is available via the Heterogeneous Tool Set HETS, which provides parsing, static analysis and proof management for heterogeneous logical theories. HETS visualises the module structure of complex logical theories, using so-called development graphs. For individual nodes (corresponding to logical theories) in such a graph, the concept hierarchy can be displayed. Moreover, HETS is able to prove intended consequences of theories, prove refinements between theories, or demonstrate their consistency. This is done by integrating several first-order provers and model-finders (SPASS, DARWIN), the higher-order prover (ISABELLE), as well as the DL reasoner PELLET.
Our contributions in this paper are: (i) we suggest a heterogeneous framework for the design of ontologies, based on the theory of institutions and the notion of development graph (Sec. 2); (ii) we supply an implementation of this framework (including reasoning support) based on the tool HETS and present a concrete syntax for SROIQ(D) that fits seamlessly into our heterogeneous approach (Sec. 3); (iii) we present a simple example showing how the structuring techniques for heterogeneous ontologies can be used in practice (Sec. 4), show how heterogeneous refinements are covered by our approach, indicate how they can be proved (automatically), and give a definition of heterogeneous sub-ontology (Sec. 5). Finally, Sec. 6 discusses future work. 2 2.1
The Common Algebraic Specification Language CASL [
A major strength of CASL is the provision of language constructs for writing modular (and heterogeneous) theories, and for the specification of refinements between theories.
The study of modularity principles can be carried
spec Prey_Animals = out to a quite large extent independently of the
sort Thing details of the underlying logical system that is
pprreedd HMaoruese :: TThhiinngg used. The notion of institutions was introduced
pred isTastier : Thing * Thing by Goguen and Burstall in the late 1970s exactly
f.oriaslTlasat,iber:T(hai,nbg) => for this purpose (see [
not isTastier (b,a) Indeed, CASL’s structuring concepts can be . iHsaTraes(tai)er/(\a,Mbo)use (b) => used for an arbitrary institution. In order to avoid end the use of category theory and to make the paFig. 1: Example in CASL per as accessible as possible, we here present the notion of an institution in an informal way.
Definition 1. An institution is a mathematical structure providing the following data: – A set of signatures, where a signature is a vocabulary of symbols. In OWL, a signature comprises a set of concept names and a set of role names. In principle, any set of objects can be used as a signature (similar remarks apply to the notions of sentences, models, and signature morphisms below). – For each signature , a set of -sentences. In OWL, sentences are the usual description logic formulas (using only concept and role names of ). – For each signature, a class of -models. -models typically provide semantic interpretations of all the symbols in . – For each signature , a satisfaction relation j= between -models and sentences. This typically is the standard Tarskian notion of truth, but non-standard notions of satisfaction (truth) can be used as well. – For each pair of signatures, a set of signature morphisms4, i.e. mappings between the signatures. In OWL, signature morphisms consist of two mappings, one for concepts and one for roles. – For each signature morphism : 1 ! 2, 1-sentences can be translated along the signature morphism: given a 1-sentence '1, its translation is written ('1). – For each signature morphism : 1 ! 2, 2-models can be reduced against the direction of the signature morphism: given a 2-model M2, its reduct is written M2 . The only condition governing institutions (i.e. the relation between the above items) is the so-called satisfaction condition, stating that truth is invariant under change of notation: M2 j= 1 '1 iff M2 j= 2 ('1) Nearly all logics occurring in practice5 can be formalised as institutions. The usual notions of logical consequence and satisfiability can be defined in an arbitrary institution. For example, given a set of -sentences and a -sentence ', we say that ' is a logical consequence of , written j= ', if all -models satisfying also satisfy '. Given a signature morphism : 1 ! 2 and a 1-model M1, a -expansion is any 2-model M2 with M2 = M1. 2.2
The advantage of the notion of institution is that it offers the possibility of defining and studying structuring constructs (and their semantics) in a way that abstracts from the details of the particular logical system. In particular, this means that we can use the same structuring constructs for both, description logics (e.g. HETDL introduced below) and first-order logic (e.g. CASL) (as well as many others, e.g. modal logic).
Tools like the heterogeneous tool set HETS do not directly work on CASL’s structuring constructs, but on a graphical translation of these, the so-called development graphs. Practically all languages for structuring and modularity can be mapped into this formalism of development graphs.
We use this notion of a development graph as a general semantic-based representation formalism for structured ontologies. The basic structuring operation for ontologies is surely that of importing other ontologies, and development graphs capture this as theory extensions. However, they also cover renaming of symbols and conservative/definitional extensions.
Definition 2. Fix an institution (which will give the semantic background for making notions such as signature, sentence, model, signature morphism and reduct precise). A development graph is an acyclic, directed graph, subject to the following conditions. Each node is decorated with a signature and a set of sentences over that signature, which together constitute the local theory of that node. This corresponds to an unstructured logical module, for example, a single OWL-DL ontology.
The links in the graph can be of different types. Global 6 definition links K represent imports of other theories; they are decorated with a signature morphism - N be4 Signature morphisms are required to form a category, that is, they can be composed and there are identity signature morphisms. 5 Non-monotonic logics can be represented by a trick that models entailments between ordinary sentences as institutions sentences. 6 There are also local and hiding definition links, which require a more refined model-theoretic semantics. tween the signatures of the involved nodes. Note that the signature morphism offers the possibility of renaming symbols while importing them.
Given a node N in a development graph DG, its associated theory ThDG (N ) is inductively defined to consist of – all the local axioms of N , and – for each global definition link K
- N 2 DG, all of ThDG (K) translated by .
The class of models ModDG (N ) of a node N is defined to consist of all models over N ’s signature that satisfy the theory ThDG (N ). tu
Complementary to definition links, which define the theories of related nodes, we also allow for theorem links with the help of which we are able to postulate relations between different theories, and hence can be seen as proof obligations, refinements, or also alignments. A (global) theorem link is an edge K ................-... N , where runs between the signatures of N and K. A development graph DG implies a theorem link K ................-... N (denoted DG j= K ................-... N ) if and only if all reducts of N -models are K-models, formally, for all M 2 ModDG (N ), M 2 ModDG (K).
A global definition (or also theorem) link K - N can be strengthened to a con- N ); it holds if every K-model has a servative extension link (denoted as K
cons expansion to an N -model. Such annotations can be seen as another kind of proof obligations. Definitional extensions are introduced in a similar way (annotated with def ); here the -expansion has to be unique. This means that a definitional extension is one where all the additional symbols in N (i.e. those not imported from K) are axiomatised (in N ) in a unique way (allowing only a unique interpretation given a K-model). By contrast, a conservative extension only requires that these symbols can be interpreted in some way.
Many languages for structuring, modularity and alignment of ontologies can be
mapped into this formalism of development graphs. Issues of modularity have been
recognised as being rather important for a while now, and have resulted in extensive research
concerning modularity principles (compare the proceedings of the workshops [15; 7; 31],
and recent work on (deciding) conservative extensions [28; 8]). We here use the term
modularity to refer to the notion of ‘ontological module’ defined through conservativity
properties, as it has been investigated for instance in [
To obtain heterogeneous logical theories, one first needs to fix some graph of logics and
logic translations, usually formalised as institutions and so-called institution comorphisms,
mapping signatures, sentences and models in a way that satisfaction is preserved, see the
discussion above and [
The so-called Grothendieck institution allows to give a semantics to heterogeneous
theories involving several institutions (see [
A HETCASL library consists of specification definitions as shown in Fig. 2.
We now briefly describe the form of HETlsopgeiccMDoLreTigers = CASL specifications, together with their trans
Tigers lation into development graphs. A specification thenIndividual: Tethys <spec> can be a basic specification consist
Type: Tiger ing of a signature and some axioms (with syntax
end DifferentFrom: Phobos, Deimos specific to the given institution). It corresponds
to a node with local axioms in a development
Fig. 2: An extension graph. A specification can be extended with
further signature elements and axioms, written
<spec> then <spec> (see Fig. 2). This leads to a definition link (decorated with
an inclusion signature morphism) in the development graph, via which the node for the
second specification imports the node for the first one. Extensions (and thereby, their
definition links) can be declared to be conservative or definitional (with semantics as
introduced above). Two specifications can be united, written <spec> and <spec>. Their
nodes are linked, again using definition links, into a new node representing the union.
Semantically, unions unite the requirements of two specifications, thereby intersecting
their model classes. Renamings, written <spec> with <signature-morphism>,
rename a specification along a signature morphism; again, this leads to a definition link in
the development graph (this time usually decorated with a non-inclusion signature
morphism). The declaration view view1: sp1 to sp2 will generate a theorem link
between the nodes representing sp1 and sp2 in the development graph. Details of the
translation to development graphs, as well as a treatment of hiding, can be found in [
We have defined a new syntax for the description logic SROIQ(D) [
Manchester Syntax at the time.
HETS. An important feature of HETDL, and its main difference to standard description logics as well as OWL 2:0, is its support for the structuring features of HETCASL, discussed in the previous section. This makes possible the heterogeneous development of and proof-support for ontologies, involving OWL as well as several other logics of different expressivity and with different semantics, in a single ontology design
A simple example for a specification in HETDL is given in Fig. 3: in it, we define two logic DL different tigers, called Phobos and Deimos, specCTliagsesr:sT=iger which are carnivores and have 4 legs. To simSubclassOf: Carnivore, plify the definition of many individuals that hasLegs exactly 4 share the same facts, HETDL introduces the Individuals: Phobos, Deimos keyword Individuals, which is used to de
TEyqpuea:liTtiyg:erDifferent fine properties for several individuals in a sinend gle block of text. Individuals has a field
Equality, which is used to declare all indiFig. 3: A simple HETDL specification viduals in the list to be the same or different. To illustrate this, consider as an example the definition in Fig. 4 on the left, which is equivalent to the longer definition in Fig. 4 on the right. The construct Individuals was introduced as a short-cut notation for the convenience of the ontology-developer.
Individuals: Phobos, Deimos, Tethys
Types: Tiger Equality: Different Individual: Phobos
Types: Tiger
DifferentFrom: Deimos, Tethys Individual: Deimos
Types: Tiger
DifferentFrom: Phobos, Tethys Individual: Tethys
Types: Tiger
DifferentFrom: Phobos, Deimos
Fig. 4: Short and longer definition of distinct individuals of the same type Of course, abstract structured heterogeneous ontologies can be formulated in different notations, and HETCASL is only one of them. Another option would be an extension of OWL with keywords dealing with corresponding structuring mechanisms.
We have designed an institution comorphism from HETDL to first-order logic (CASL).
This comorphism is designed along OWL 2:0’s model-theoretic semantics, adapted to the
structuring of HETDL specifications. The translation provided is essentially the same as
the standard-translation to first-order logic, with the minor difference that we translate into
a many-sorted first-order variant—see [
SubclassOf: hasClaws some Claws This will be translated to a sentence and a predicate declaration. The expression Class: Tiger yields the declaration pred Tiger : Thing. Then, SubclassOf: hasClaws some Claws is translated to 8 x : Thing . Tiger(x) =) JhasClaws some ClawsK (x), where JsK denotes the mapping of the concept s along the comorphism. Note that the class Tiger is used in the formula for the subclass definition. More generally, all statements following one of the keywords Class, ObjectProperty, DataProperty, and Individual(s), are treated in this way, until the next keyword of this type is reached.
After having discussed the theory of heterogeneous ontologies in some detail in Sec. 2.3, we now illustrate how to define an ontology heterogeneously from 3 parts formalised in different languages. Firstly, consider a basic specification written in HETDL, given in Fig. 5 on the left hand side, describing Tigers being carnivores and cats of prey. logic DL spec Predators =
Class: Carnivore end
Class: Tiger
SubclassOf: Carnivore,
CatsOfPrey logic CASL spec Prey =
Prey_Animals then %implies forall a,b : Thing . Hare(a) /\ Mouse (b) => not isTastier (b,a) end
Secondly, consider another basic specification in CASL (please remember that Prey_Animals is given in Fig. 1) describing their prey, given in Fig. 5 on the right hand side. The keyword %implies here introduces a proof obligation, namely a theorem link expressing that the part after %implies logically follows from the parts before. This particular proof obligation follows from the asymmetry of isTastier specified in Fig. 1. Such annotations can be quite useful for an ontology designer as a control mechanism to keep track of desired consequences: in case such a proof obligation fails, a design error has been made. Thirdly, consider the specification below: logic CASL spec Animals =
Predators and {Prey with Hare |-> Lepus}
then
pred prefers : Thing * Thing * Thing
forall a,b,c : Thing
. Tiger(a) /\ isTastier (b,c) <=> prefers (a,b,c)
then %implies
forall a,b,c : Thing
. Tiger(a) /\ Lepus(b) /\ Mouse (c) => prefers (a,b,c)
end
is formalised in a DL, thus allowing it to be proved by a DL reasoner. With this approach,
many ‘conjectures’ can already be proven in a smaller, ‘local’ environment. Further, this
approach helps the designer of an ontology to find inconsistencies: if the overall ontology
turns out to be inconsistent, it is possible to check the consistency of the theories of all
nodes in the development graph that contribute to the overall specification. If one of them
turns out to be inconsistent, it might already be possible to fix the inconsistency in this
smaller, local theory. Note that this ‘scales down’ the search space for finding
inconsistencies in a way that is independent from the techniques developed in [
When comparing different ontologies it is of interest whether all axioms of an ontology
O1 are also entailed by another (larger or more complex) ontology O2. This is formalised
via the notion of refinement adapted from software engineering [
Proposition 5. For a heterogeneous refinement, any O2-model can be translated to an O1model, and moreover, logical consequence is preserved along refinement: for ( (')) = ( ), O1 j= ' implies O2 j= ( ).
Definition 6. We call an ontology O1 a (heterogeneous) sub-ontology of O2 if and only if
O2 is a (heterogeneous) refinement of O1.
8 There are other usages of the term ‘refinement’ in the DL literature, e.g. in concept learning [
ObjectProperty: isFaster
Characteristics: Transitive, Irreflexive Class: Cheetah
SubclassOf: Carnivore, isFaster some Tiger
DisjointWith: Tiger end
Class: Tiger
SubclassOf: Carnivore DisjointWith: Cheetah MoreCats
Cats and another ontology of these animals given in CASL and containing more information: logic CASL spec MoreCats = pred Cheetah, Tiger, Lion : Thing pred isFaster : Thing * Thing pred Carnivore : Thing forall a,b,c :Thing . Cheetah (a) => Carnivore (a) . Tiger (a) => Carnivore (a) . Lion (a) => Carnivore (a) . Cheetah(a) => exists b : Thing . isFaster(a,b) /\ Tiger(b) . Tiger(a) => exists b : Thing . isFaster(a,b) /\ Lion(b) . not (Tiger(a) /\ Cheetah(a)) . not (Tiger(a) /\ Lion(a)) . not (Lion(a) /\ Cheetah(a)) . not isFaster(a, a) . isFaster(a, b) /\ isFaster(b, c) => isFaster(a, c) end One can easily see that there is in fact a signature inclusion morphism from Cats to MoreCats. To create a proof obligation that covers the fact that MoreCats might be a refinement of Cats, a heterogeneous view in CASL is introduced: logic CASL view cview : Cats to MoreCats
Again, we can easily see that all models of MoreCats are models of Cats if we reduce the signature to forget the Lion. By Def. 4, MoreCats is a heterogeneous refinement of Cats, while Cats is a sub-ontology of MoreCats. In HETS, this refinement is displayed as in Fig. 8 on the right. 6
We have introduced an abstract framework for the study of structured heterogeneous ontologies, allowing for a systematic analysis of conceptual and algorithmic problems in heterogeneous environments that were previously considered rather disparate. We have pointed out a way for ontology designers to build their ontologies in a heterogeneous and structured fashion, splitting it up in several meaningful modules and plugging them together to make up the overall ontology. With this heterogeneous approach it is possible to define parts of an ontology in several logics depending on the needed expressivity. The mantra of this approach is: as simple as possible, as expressive as needed.
We have given a notion of heterogeneous refinement providing a very strong relation between two ontologies, and shown that it is directly supported within our framework. With this notion, we can determine if an ontology is a sub-ontology of another, larger or more complex one and which might be specified in a different formalism. This provides a convenient tool for the comparison of ontologies.
Unlike related approaches like Common Logic [
The structured reasoning support that our approach allows has already been used for
answering questions that ‘standard’ automated reasoning can not tackle: the consistency
of the first-order version of the foundational ontology DOLCE (reformulated as a
HETCASL specification) can be verified by model-checking a view into a finite specification of
a model for DOLCE, and the structuring techniques built into HETS also support the
modular construction of models for large first-order ontologies such as DOLCE [
Currently, we are working on integrating a tool for the discovery of theory morphisms into the Heterogeneous Tool Set as well as on integrating modularisation algorithms as developed in [21; 8]. These techniques would allow (semi)-automatic structuring of ontologies and the discovery of ontology overlaps modulo alignment mappings.
Work on this paper has been supported by the DFG-funded collaborative research centre SFB/TR 8 Spatial Cognition and by the German Federal Ministry of Education and Research (Project 01 IW 07002 FormalSafe). We thank John Bateman, Mihai Codescu, Alexander Garcia Castro, Joana Hois, and Lutz Schro¨der for fruitful discussions, the anonymous reviewers for constructive comments, and Erwin R. Catesbeiana for insights into conservativity issues.