×

Pay-as-you-go description logic reasoning by coupling tableau and saturation procedures. (English) Zbl 1347.68326

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
Full Text: DOI