Reasoning for Expressive Ontology Languages

Ontologies, and ontology based vocabularies, have become increasingly important. They provide a common vocabulary together with computer-accessible descriptions of the meaning of relevant terms and relationships between these terms. Ontologies play a major role in the Semantic Web and in e-Science where they are widely used in, e.g., bio-informatics, medical terminologies and other knowledge management applications.

One of the most important aspect of ontologies is that they contain knowledge structured in a special way. The users of ontologies are typically interested in obtaining information about relationships between concepts described in ontologies and querying the ontologies. Both tasks require reasoning tools: tools that can derive new knowledge from the ontological knowledge.

To represent knowledge in ontologies, one often needs very expressive languages. Reasoning with such languages is a very hard combinatorial problem, and existing reasoning tools can be ineffective on realistic ontologies, particularly those used in e-Science applications. Moreover, such applications often need more expressive languages than those supported by existing tools. The aim of this project was, therefore, to develop new methods of reasoning with large ontologies using very expressive languages, to implement these methods in a new reasoning system, and to demonstrate its effectiveness.

In order to improve the performance of reasoning tools, we developed a new calculus related to the hypertableau and hyperresolution calculi known from FOL theorem proving. In addition, we developed a range of new optimisation techniques for use with this calculus. Compared to existing tableau based techniques, the optimised "hypertableau" calculus reduces both nondeterminism and model size, making it much more effective with complex ontologies of the kind often used in e-Science applications.

In order to satisfy application requirements for even more expressive languages, we developed a new representation formalism that extends expressive DLs with "description graphs"; these allow for the faithful representation of complex physical structures of the kind found in many e-Science applications, e.g., in the representation of anatomy. Moreover, we showed that the standard reasoning problems are still decidable for ontologies that satisfy some simple syntactic restrictions, and that a decision procedure can be implemented as an extension of our new hypertableau calculus. In case the input ontology does not satisfy the relevant restrictions, the extended calculus can still be used for reasoning as it allows for the identification of situations in which it will be incomplete.

In addition to developing new reasoning procedures, we have also developed a theoretically well founded technique for ontology modularisation. The properties of the resulting modules mean that they can be used both to optimise reasoning techniques (e.g., by allowing reasoners to working on small subsets of the ontology) and to allow different reasoning techniques to be used on different parts of the ontology. Modules can also be used to support incremental reasoning, i.e., recomputing cached inferences only as necessary when an ontology is modified.

We have implemented our (extended) calculus in the HermiT reasoner. In case studies using very large ontologies from e-Science applications we have demonstrated that it outperforms existing reasoners in almost all cases, and in some cases is the only reasoner able to deal with complex ontologies (e.g., the original version of the GALEN medical terminology ontology).

Finally, we studied a number of other language extensions and reasoning techniques. Our results include the development of a new resolution-based calculus for expressive DLs, a decision procedure for languages extended with role conjunction, and new complexity results for languages supporting expressive role inclusion axioms.