=Paper=
{{Paper
|id=Vol-432/paper-9
|storemode=property
|title=The OWL in the CASL - Designing Ontologies Across Logics
|pdfUrl=https://ceur-ws.org/Vol-432/owled2008eu_submission_27.pdf
|volume=Vol-432
|dblpUrl=https://dblp.org/rec/conf/owled/KutzLMN08
}}
==The OWL in the CASL - Designing Ontologies Across Logics==
https://ceur-ws.org/Vol-432/owled2008eu_submission_27.pdf
The OWL in the C ASL
Designing Ontologies Across Logics
Oliver Kutz1 , Dominik Lücke1 , Till Mossakowski1,2 , and Immanuel Normann3
1
SFB/TR 8 Spatial Cognition, University of Bremen, Germany
{okutz,luecke,till}@informatik.uni-bremen.de
2
DFKI GmbH Bremen, Germany
Till.Mossakowski@dfki.de
3
Department of Linguistics, University of Bremen, Germany
normann@uni-bremen.de
Abstract. In this paper, we show how the web ontology language OWL can be ac-
commodated within the larger framework of the heterogeneous common algebraic
specification language H ET C ASL. Through this change in perspective, OWL can
benefit from various useful H ET C ASL 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 C ASL, 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 auto-
mated reasoning support for different logics.
1 Introduction
Ontologies play an increasingly important role in various areas of Knowledge Represen-
tation, 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 SHOIN (D) (under-
lying OWL-DL) and SROIQ(D) (underlying OWL 2.0). These logics are characterised
by having a rather fine-tuned expressivity, exhibiting (still) decidable satisfiability prob-
lems, whilst being amenable to highly optimised implementations.
However, there are many cases where either weaker DLs are enough, such as sub-
Boolean EL, 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 [33], an ex-
ample for the latter many foundational ontologies, for instance D OLCE [12] and GUM
[3].
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 [19]. Also, sim-
ple operations such as the re-use of parts of an ontology in a different ‘context’ whilst
renaming (parts of) the signature are not possible in the OWL languages.
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 ontol-
ogy, 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 mean-
ingful 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 (ex-
tensions) 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 de-
sired 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 ontol-
ogy 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 founda-
tional 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 per-
spective as so-called institutions [13] and supply institution comorphisms as mappings
between them, including the DL SROIQ(D) and many-sorted first-order logic (using
the language C ASL).
Tool support for developing heterogeneous ontologies is available via the Heteroge-
neous Tool Set H ETS, which provides parsing, static analysis and proof management for
heterogeneous logical theories. H ETS visualises the module structure of complex logical
theories, using so-called development graphs. For individual nodes (corresponding to log-
ical theories) in such a graph, the concept hierarchy can be displayed. Moreover, H ETS 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 (S PASS, DARWIN), the higher-order prover (I SABELLE), as well as the DL
reasoner P ELLET.
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 reason-
ing support) based on the tool H ETS and present a concrete syntax for SROIQ(D) that
fits seamlessly into our heterogeneous approach (Sec. 3); (iii) we present a simple ex-
ample 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 Structuring, Modularity, and Heterogeneity for Ontologies
2.1 C ASL and Institution Theory
The Common Algebraic Specification Language C ASL [4, 6] provides a user-friendly
notation for first-order logic, much in the same way that H ET DL (see below) and Manch-
ester syntax provide a user-friendly notation for OWL-DL. A sample C ASL specification
is shown in Fig. 1.
A major strength of C ASL 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
pred Hare : Thing
pred Mouse : Thing used. The notion of institutions was introduced
pred isTastier : Thing * Thing by Goguen and Burstall in the late 1970s exactly
forall a,b :Thing
. isTastier (a,b) => for this purpose (see [13]).
not isTastier (b,a) Indeed, C ASL’s structuring concepts can be
. Hare(a) /\ Mouse (b) =>
isTastier (a,b) used for an arbitrary institution. In order to avoid
end the use of category theory and to make the pa-
Fig. 1: Example in C ASL 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 descrip-
tion logic formulas (using only concept and role names of Σ).
– For each signature, a class of Σ-models. Σ-models typically provide semantic inter-
pretations of all the symbols in Σ.
– For each signature Σ, a satisfaction relation |=Σ 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σ |=Σ1 ϕ1 iff M2 |=Σ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 Γ |= ϕ, 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 Development Graphs for Structuring and Modularity
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 de-
tails of the particular logical system. In particular, this means that we can use the same
structuring constructs for both, description logics (e.g. H ET DL introduced below) and
first-order logic (e.g. C ASL) (as well as many others, e.g. modal logic).
Tools like the heterogeneous tool set H ETS do not directly work on C ASL’s structuring
constructs, but on a graphical translation of these, the so-called development graphs. Prac-
tically 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 representa-
tion 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 no-
tions such as signature, sentence, model, signature morphism and reduct precise). A de-
velopment 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 to-
gether 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 N
represent imports of other theories; they are decorated with a signature morphism σ be-
4
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 in-
ductively defined to consist of
– all the local axioms of N , and
σ -
– for each global definition link K N ∈ 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 ). t
u
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 be-
tween 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 |= K ...................
- N ) if and only if all reducts of N -models are K-models,
formally, for all M ∈ ModDG (N ), Mσ ∈ ModDG (K).
σ
- N can be strengthened to a con-
A global definition (or also theorem) link K
σ -
servative extension link (denoted as K N ); it holds if every K-model has a σ-
cons
expansion to an N -model. Such annotations can be seen as another kind of proof obliga-
tions. 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 recog-
nised 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 mod-
ularity to refer to the notion of ‘ontological module’ defined through conservativity proper-
ties, as it has been investigated for instance in [20, 8, 25], and the term structuring for the
systematic combination of (possibly heterogeneous) ontologies through (not necessarily
conservative) operations such as union, extension, etc. The verification of conservativi-
ties, or the check of syntactic ‘safety’ conditions for conservativity, is accomplished from
within the tool H ETS, employing corresponding algorithmic approaches.
2.3 Heterogeneous Ontologies and H ET C ASL
Since ontologies are being written in many different formalisms, like description logics,
first-order logic, and modal (first-order) logics, combinations of ontologies need to be
constructed across different institutions, as is argued convincingly in [32].
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 [14] for further details.
The so-called Grothendieck institution allows to give a semantics to heterogeneous
theories involving several institutions (see [9, 29]). Basically, it is a flattening, or disjoint
union, of the logic graph. A signature in the Grothendieck institution is a pair consisting
of a logic (institution) and a signature in that logic. Similarly, a Grothendieck signature
morphism consists of a logic translation plus a signature morphism (in the target logic).
Sentences, models and satisfaction in the Grothendieck institution are defined componen-
twise. We now arrive at the following:
Definition 3. An abstract structured heterogeneous ontology (w.r.t. some logic graph) is
a node O in a development graph DG in the corresponding Grothendieck institution.
(We sometimes also identify O with its theory ThDG (O); however, note that then the
structuring is lost.) To be able to write down such heterogeneous ontologies in a con-
cise manner, we extend C ASL to H ET C ASL as follows: H ET C ASL provides the notation
logic , which defines the institution of the following specifications
until that keyword occurs again. Also, a specification can be translated along a comor-
phism; this is written with logic .
A H ET C ASL library consists of specification definitions as shown in Fig. 2.
We now briefly describe the form of H ET-
logic DL
spec MoreTigers =
C ASL specifications, together with their trans-
Tigers lation into development graphs. A specification
then
Individual: Tethys
can be a basic specification consist-
Type: Tiger ing of a signature and some axioms (with syntax
DifferentFrom: Phobos, Deimos
end
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
then (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 def-
inition links) can be declared to be conservative or definitional (with semantics as intro-
duced above). Two specifications can be united, written and . 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 with ,
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 mor-
phism). 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 [30].
3 H ET DL: A spawn of Manchester Syntax for OWL
We have defined a new syntax for the description logic SROIQ(D) [18], called H ET DL
(Heterogeneous DL), which is based on the Manchester Syntax for OWL 1.0 [16] and
which has been developed in parallel to the Manchester Syntax for OWL 2.0 [17].7 A
grammar for H ET DL is supplied via a technical report [23]; tool support is offered via
7
The main reason for this parallel development was the lack of a complete formal grammar for the
Manchester Syntax at the time.
H ETS. An important feature of H ET DL, and its main difference to standard description
logics as well as OWL 2.0, is its support for the structuring features of H ET C ASL, dis-
cussed 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 H ET DL is given in Fig. 3: in it, we define two
logic DL different tigers, called Phobos and Deimos,
spec Tigers =
Class: Tiger which are carnivores and have 4 legs. To sim-
SubclassOf: Carnivore, plify the definition of many individuals that
hasLegs exactly 4
share the same facts, H ET DL introduces the
Individuals: Phobos, Deimos keyword Individuals, which is used to de-
Type: Tiger
Equality: Different fine properties for several individuals in a sin-
end gle block of text. Individuals has a field
Equality, which is used to declare all indi-
Fig. 3: A simple H ET DL specification viduals in the list to be the same or different. To
illustrate this, consider as an example the defini-
tion 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 Individual: Phobos
Types: Tiger Types: Tiger
Equality: Different 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 H ET C ASL 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 H ET DL to first-order logic (C ASL).
This comorphism is designed along OWL 2.0’s model-theoretic semantics, adapted to the
structuring of H ET DL 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 [23] for full details. Consider a subsumption like:
Class: Tiger
SubclassOf: hasClaws some Claws
This will be translated to a sentence and a predicate declaration. The expres-
sion Class: Tiger yields the declaration pred Tiger : Thing. Then,
SubclassOf: hasClaws some Claws is translated to ∀ 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.
4 Plugging things together: A heterogeneously structured ontology
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 H ET DL, given in
Fig. 5 on the left hand side, describing Tigers being carnivores and cats of prey.
logic DL logic CASL
spec Predators = spec Prey =
Class: Carnivore Prey_Animals
then %implies
Class: Tiger forall a,b : Thing
SubclassOf: Carnivore, . Hare(a) /\ Mouse (b) => not isTastier (b,a)
CatsOfPrey end
end
Fig. 5: Predators and their prey
Secondly, consider another basic specification in C ASL (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 theo-
rem 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 mecha-
nism 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
This is the union of the above ones and adds a new 3-ary predicate that cannot
directly be expressed in SROIQ(D). In the pro-
cess of uniting the specifications, Predators is
mapped along the comorphism from H ET DL to
Prey Predators
C ASL. Further, Hare is being renamed to Lepus.
The development graph of this heterogeneous spec-
ification is displayed in H ETS as shown in Fig. 6.
Animals Please note that the solid black arrows depict defini-
tion links (the double-lined arrows indicate hetero-
geneous definition links), whilst the light green ar-
rows are theorem links (and the dotted green arrows
local theorem links introduced by the development
graph calculus [30]). The unnamed nodes, which
contain the proof obligations, can now be proved
by running a theorem-prover on them, i.e., on their
local theories. This way, we do not have to deal with
axioms that are introduced later and that are not im-
portant for this theory. Please note that the theory of
Fig. 6: Development Graph of the Het-
erogeneous specification
the unnamed node with a theorem link from Prey
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 inconsisten-
cies in a way that is independent from the techniques developed in [19].
5 Heterogeneous Refinements and Sub-Ontologies
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 [11]. Note that since we
do not assume that O2 is a superset of O1 (by ‘larger’ we simply mean ‘greater number
of axioms’), deciding refinements is in general non-trivial.8 A new notion in the area of
ontology design is that of a heterogeneous refinement that covers the important case where
different logics are involved; it is formalised as follows:
Definition 4. Given two ontologies O1 and O2 in the same logic, we call O2 a refinement
σ
of O1 if there is a theorem link O1 −→ O2 that follows from the underlying development
graph. Now let ontologies O1 and O2 in logics LO1 and LO2 be given, such that there
θ η
is a logic L with comorphisms LO1 −→ L and LO2 −→ L, where η is conservative.
The translations of the ontologies along the comorphism are referred to as O1 0 and O2 0 .
σ
We call O2 a heterogeneous refinement of O1 if there is a theorem link O10 −→ O20 that
follows from the underlying development graph.
Proposition 5. For a heterogeneous refinement, any O2 -model can be translated to an O1 -
model, and moreover, logical consequence is preserved along refinement: for σ(θ(ϕ)) =
η(ψ), O1 |= ϕ implies O2 |= η(ψ).
σ Fig. 7 depicts a heterogeneous refine-
O10 .................................
- O20
ment as defined in Def. 4. In H ET C ASL,
θ6 c6
η
this concept is addressed by the notion of
view creating a proof obligation, as dis-
O1 O2
cussed in Sec. 2.
Our abstract definition of refinement
Fig. 7: A refinement Diagram. entails the common definition in software
engineering: consider O1 to be a specifica-
tion of a program in an algebraic specification language, and O2 its implementation in a
programming language. Refinements are a common problem in the world of ontologies
as well: establish whether a domain ontology is consistent with respect to the knowledge
represented in a foundational ontology. The notion of refinement leads us to the definition
of heterogeneous sub-ontologies.
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 [26].
5.1 A Very Simple Heterogeneous Refinement: Cats
We will clarify the notion of heterogeneous refinement with an example. Consider a small
ontology dealing with cats of prey in H ET DL:
logic DL
spec Cats =
ObjectProperty: isFaster
Characteristics: Transitive, Irreflexive
Class: Cheetah
SubclassOf: Carnivore, isFaster some Tiger
DisjointWith: Tiger
Class: Tiger
SubclassOf: Carnivore
MoreCats Cats
DisjointWith: Cheetah
end
Fig. 8: Heterogeneous Refinement
and another ontology of these animals given in C ASL 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 C ASL 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 refine-
ment of Cats, while Cats is a sub-ontology of MoreCats. In H ETS, this refinement is
displayed as in Fig. 8 on the right.
6 Discussion and Future Work
We have introduced an abstract framework for the study of structured heterogeneous on-
tologies, 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 to-
gether 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 [27], our approach provides explicit
structuring mechanisms, and logic translations are treated as first-class citizens. Of course,
it is also possible without too much effort to add Common Logic as another logic to the
H ETS logic graph.
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 D OLCE (reformulated as a H ET-
C ASL specification) can be verified by model-checking a view into a finite specification of
a model for D OLCE, and the structuring techniques built into H ETS also support the mod-
ular construction of models for large first-order ontologies such as D OLCE [22]. We also
work on determining the exact logical relationship between different versions of D OLCE,
formalised in various DLs as well as first-order logic: here, only partial heterogeneous
refinements can be established as the DL versions are hand-made approximations of the
first-order version.
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 on-
tologies and the discovery of ontology overlaps modulo alignment mappings.
Acknowledgements
Work on this paper has been supported by the DFG-funded collaborative research cen-
tre 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 Schröder for fruitful discussions, the
anonymous reviewers for constructive comments, and Erwin R. Catesbeiana for insights
into conservativity issues.
Bibliography
[1] A. Artale and E. Franconi. A survey of temporal extensions of description logics. Annals of
Mathematics and Artificial Intelligence, 30(1-4):171–210, 2000.
[2] A. Artale, R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev. Temporalising tractable
description logics. In Proc. of the 14th Int. Symposium on Temporal Representation and Rea-
soning (TIME), pages 11–22, Washington, DC, USA, 2007. IEEE.
[3] J. Bateman, T. Tenbrink, and S. Farrar. The Role of Conceptual and Linguistic Ontologies in
Discourse. Discourse Processes, 44(3):175–213, 2007.
[4] M. Bidoit and P. D. Mosses. C ASL User Manual. LNCS Vol. 2900. Springer, 2004.
[5] D. Calvanese, D. Lembo, M. Lenzerini, and R. Rosati. Epistemic first-order queries over
description logic knowledge bases. In In Proc. DL 2006, Lake District, UK, May 30June, page
2006.
[6] CoFI (The Common Framework Initiative). C ASL Reference Manual. LNCS Vol. 2960.
Springer, 2004.
[7] B. Cuenca Grau, V. Honavar, A. Schlicht, and F. Wolter, editors. 2nd International Workshop on
Modular Ontologies (WoMO-07), volume 315, (K-CAP) Whistler, BC, Canada, 2007. CEUR
Workshop Proceedings.
[8] B. Cuenca Grau, I. Horrocks, Y. Kazakov, and U. Sattler. Modular Reuse of Ontologies: Theory
and Practice. J. of Artificial Intelligence Research (JAIR), 31, 2008.
[9] R. Diaconescu. Grothendieck Institutions. Applied Categorical Structures, 10:383–402, 2002.
[10] F. M. Donini, M. Lenzerini, D. Nardi, W. Nutt, and A. Schaerf. An epistemic operator for
description logics. Artif. Intell., 100(1-2):225–274, 1998.
[11] H. Ehrig and H.-J. Kreowski. Refinement and implementation. In E. Astesiano, H.-J. Kreowski,
and B. Krieg-Brückner, editors, Algebraic Foundations of Systems Specifications, pages 201–
242. Springer Verlag, 1999.
[12] A. Gangemi, N. Guarino, C. Masolo, A. Oltramari, and L . Schneider. Sweetening Ontologies
with DOLCE. In Proc. of EKAW 2002, LNCS Vol. 2473, pages 166–181. Springer, 2002.
[13] J. A. Goguen and R. M. Burstall. Institutions: Abstract Model Theory for Specification and
Programming. Journal of the ACM, 39:95–146, 1992.
[14] J. A. Goguen and G. Roşu. Institution morphisms. Formal Aspects of Computing, 13:274–307,
2002.
[15] P. Haase, V. Honavar, O. Kutz, Y. Sure, and A. Tamilin, editors. 1st Int. Workshop on Modular
Ontologies (WoMO-06), volume 232, (ISWC) Athens, Georgia, USA, 2006. CEUR Vol. 232.
[16] M. Horridge, N. Drummond, J. Goodwin, A. Rector, R. Stevens, and H. Wang. The Manchester
OWL Syntax. In OWL: Experiences and Directions, 2006.
[17] M. Horridge and P. Patel-Schneider. Manchester Syntax for OWL 1.1. In OWL: Experiences
and Directions, Washington, DC, 2008.
[18] I. Horrocks, O. Kutz, and U. Sattler. The Even More Irresistible SROIQ. In Proc. of KR,
pages 57–67, 2006.
[19] A. Kalyanpur, B. Parsia, M. Horridge, and E. Sirin. Finding all Justifications of OWL DL
Entailments. In Proc. of ISWC/ASWC2007, LNCS Vol. 4825, pages 267–280. Springer, 2007.
[20] B. Konev, C. Lutz, D. Walther, and F. Wolter. Formal properties of modularization. In H. Stuck-
enschmidt and S. Spaccapietra, editors, Ontology Modularization. Springer, 2008.
[21] B. Konev, C. Lutz, D. Walther, and F. Wolter. Semantic Modularity and Module Extraction in
Description Logics. In 18th European Conf. on Artificial Intelligence (ECAI-08), 2008.
[22] O. Kutz, D. Lücke, and T. Mossakowski. Modular Construction of Models—Towards a Consis-
tency Proof for the Foundational Ontology D OLCE. In 1st Int. Workshop on Computer Science
as Logic-Related, ICTAC 2008, Istanbul, Turkey, 2008.
[23] O. Kutz, D. Lücke, T. Mossakowski, and I. Normann. The OWL in the C ASL. Technical report,
University of Bremen, Bremen, Germany http://www.informatik.uni-bremen.
de/˜okutz/OWLinCASL-TR.pdf, 2008.
[24] O. Kutz, C. Lutz, F. Wolter, and M. Zakharyaschev. E-connections of abstract description
systems. Artificial Intelligence, 156(1):1–73, 2004.
[25] O. Kutz and T. Mossakowski. Conservativity in Structured Ontologies. In 18th European Conf.
on Artificial Intelligence (ECAI-08). IOS Press, 2008.
[26] J. Lehmann and P. Hitzler. Foundations of refinement operators for description logics. In Proc.
of the 17th Int. Conf. on Inductive Logic Programming (ILP), volume 4894 of LNCS, pages
161–174. Springer, 2008.
[27] Common Logic. http://common-logic.org/.
[28] C. Lutz, D. Walther, and F. Wolter. Conservative Extensions in Expressive Description Logics.
In Proceedings of IJCAI-07, pages 453–458. AAAI Press, 2007.
[29] T. Mossakowski. Comorphism-based Grothendieck logics. In Mathematical Foundations of
Computer Science, volume 2420 of LNCS, pages 593–604. Springer, 2002.
[30] T. Mossakowski, S. Autexier, and D. Hutter. Development Graphs—Proof Management for
Structured Specifications. J. of Logic and Algebraic Programming, 67(1–2):114–145, 2006.
[31] U. Sattler and A. Tamilin, editors. Workshop on Ontologies: Reasoning and Modularity
(WORM-08), volume 348, ESWC, Tenerife, Spain, 2008. CEUR Workshop Proceedings.
[32] M. Schorlemmer and Y. Kalfoglou. Institutionalising Ontology-Based Semantic Integration.
Journal of Applied Ontology., 2008. To appear.
[33] N. Sioutos, S. de Coronado, M. W. Haber, F. W. Hartel, W.-L. Shaiu, and L. W. Wright. NCI
Thesaurus: A semantic model integrating cancer-related clinical and molecular information.
Journal of Biomedical Informatics, 40(1):30–43, 2007.