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, necessitating an in-depth understanding of the concepts of modularity and formal structuring as applied to ontologies.

Therefore, together with Till Mossakowski, Dominik Lücke, and Mihai Codescu, we are analysing in detail the application of formal structuring methods as deployed in algebraic formal specification in software engineering to ontologies. In particular, we employ the Heterogeneous Tool Set HETS for bringing these techniques into the world of ontological engineering.

With Joana Hois, I also study the problem of applying these structuring techniques to ontologies intended to capture (spatial) natural language semantics and the combination of such ontologies with spatial calculi.

With Corinna Elsenbroich and Ulrike Sattler, I have started working on abductive reasoning techniques for ontologies. This is a very interesting area from an application point of view as abduction can be used to define new, and highly useful, reasoning tasks over ontologies. Prominent application areas include diagnosis using medical ontologies or problems in spatial navigation. A first paper can be found here.

Together with Ian Horrocks and Ulrike Sattler, I have been working on extending the expressivity of the description logic SHOIN underlying the web ontology language OWL-DL.

We defined a logic, called SROIQ, that adds numerous expressive means that were suggested to us by ontology developers as useful additions to OWL-DL, making it more useful in practise. SROIQ is carefully designed to remain decidable and, in particular, to be efficiently implementable building on the succesful implementations of reasoners such as FaCT++.

The logic SROIQ has been adopted as the logical basis for the first successor to OWL, OWL 1.1.

The theory of E-connections, developed jointly with Carsten Lutz, Frank Wolter, and Michael Zakharyaschev, is a methodology for combining knowledge representation and reasoning formalisms that is rather expressive, natural from a semantical point of view, and which is very well-behaved computationally in the sense that the combination of decidable formalisms is again decidable, and which, nonetheless, allows non-trivial interactions between the combined components.

In E-connections, a finite number of formalisms are `connected' by relations relating entities across different domains, intended to capture different aspects or representations of the `same object'. For instance, an `abstract' object of a description logic can be related via a relation R to its life-span in a temporal logic as well as to its spatial extension in a spatial logic.

E-connections have attracted several researchers worldwide, and it has been realised that besides their original purpose as a powerful framework for integrating logical formalisms of diverse characteristics, they also have great potential as a formalism employed in the Semantic Web, in particular concerning the problem of modularity for web ontologies.

Working with Holger Sturm, Nobu-Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev, I studied Logics of Distance. These are modal (hybrid) logics whose modal operators introduce a quantitative notion of distance or similarity, thus widening the scope of the typically `qualitative' spatial representation and reasoning.

Such a distance operator would say, for instance, that everywhere at distance less or equal r (a rational number), formula φ holds. We found decidable distance logics, investigated their complexity, axiomatisations, and logical properties like interpolation.

Besides applications in spatial reasoning, these logics can also be interpreted as dealing with similarity measures (inducing a distance function) which are ubiquitous in Knowledge Representation. For instance, similarity measures appear naturally in an analysis of definitions of concepts by prototypes, or in the classification of proteins in Bioinformatics.

Together with Marcus Kracht, I have been investigating various semantics for languages of modal predicate logics that combine modalities (such as `possibility' and `necessity') with first-order quantification over individuals.

These languages are notorious for the semantic difficulties they pose, and their investigation has a long and tangled history. We are particularly interested in finding general but still `natural' semantics, and in an analysis of the different notions of world, accessibility, and object. Interesting applications include, for instance, an analysis of notions of persistence through time, or ontologies of space-time theories, and the progress made in the area (in particular concerning decidable fragments) has revived an interest in these languages also as knowledge representation formalisms. Specifically, the development of so-called `generalised counterpart-theoretic semantics' in this context directly influenced the development of E-connections.

A summary of our work can be found in this recent paper.