Optimisation of tableau-based reasoning systems for expressive description logics

Logic-based knowledge representation formalisms, such as Description Logics, constitute the basis of well-known ontology languages, e.g., the Web Ontology Language, and, thus, are gaining more and more popularity for realising the knowledge and information handling of intelligent systems in various disciplines, e.g., life sciences, medical informatics, the Semantic Web. A particular strength of such logical formalisms is that automated reasoning systems can be used to derive logically implied consequences of the explicitly represented knowledge. Although expressive representation formalisms provide many modelling constructors to represent application domains in detail, they require sophisticated reasoning procedures, such as tableau algorithms, which systematically try to build counter examples in order to refute statements w.r.t. the represented knowledge. In this thesis, we present a range of new optimisation techniques for such tableau-based reasoning systems, which improve the reasoning performance especially for more expressive Description Logics. First, we propose a new absorption technique, where axioms are rewritten such that the non-deterministic processing within the reasoning system is notably reduced. We further extend absorption to enable an efficient handling of so-called nominal schemas, which even allow for expressing arbitrary rule-based knowledge. In addition, we present a tight coupling of tableau algorithms with saturation procedures, which enables a very efficient derivation of many consequences and, thus, results in a pay-as-you-go behaviour, i.e., the reasoning system can dynamically process all those parts very efficiently that are not directly influenced by expressive modelling constructors. Last but not least, we present different caching and parallelisation techniques, which primarily address reasoning with many facts. We integrated the developed optimisation techniques into a new, freely available reasoning system called Konclude and our evaluation with several thousand ontologies shows that these optimisations lead to new performance standards. These results have also been confirmed by international competitions, where Konclude was able to win several awards