Steigmiller, Andreas; Glimm, Birte Pay-as-you-go description logic reasoning by coupling tableau and saturation procedures. (English) Zbl 1347.68326 J. Artif. Intell. Res. (JAIR) 54, 535-592 (2015). Summary: Nowadays, saturation-based reasoners for the OWL EL profile of the Web Ontology Language are able to handle large ontologies such as SNOMED very efficiently. However, it is currently unclear how saturation-based reasoning procedures can be extended to very expressive Description Logics such as \(\mathcal{SROIQ}\) – the logical underpinning of the current and second iteration of the Web Ontology Language. Tableau-based procedures, on the other hand, are not limited to specific Description Logic languages or OWL profiles, but even highly optimised tableau-based reasoners might not be efficient enough to handle large ontologies such as SNOMED. In this paper, we present an approach for tightly coupling tableau- and saturation-based procedures that we implement in the OWL DL reasoner Konclude. Our detailed evaluation shows that this combination significantly improves the reasoning performance for a wide range of ontologies. MSC: 68T30 Knowledge representation 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68T27 Logic in artificial intelligence Software:Konclude PDFBibTeX XMLCite \textit{A. Steigmiller} and \textit{B. Glimm}, J. Artif. Intell. Res. (JAIR) 54, 535--592 (2015; Zbl 1347.68326) Full Text: DOI