Parallelizing Tableaux-Based Description Logic Reasoning

Practical scalability of Description Logic (DL) reasoning is an important premise for the adoption of OWL in a real-world setting. Many highly efficient optimizations for the DL tableau calculus have been invented over the last decades. None of them aimed at parallelizing the tableau algorithm itself. This paper describes our approach for concurrent computation of the nondeterministic choices inherent to the standard tableau procedure. We discuss how this interrelates with the well-known optimization techniques and present first promising performance results when benchmarking our prototypical reasoner UUPR (Ulm University Parallel Reasoner) with a selection of established DL systems. 1 Motivation Tableaux-based algorithms have shown to be an adequate method in order to implement Description Logic (DL) reasoning services for many practical usecases of moderate size. However, scalability of OWL reasoning is still an actual challenge of DL research [6]. Recent optimizations have shown si...

• Type: Conference
• Year: 2007
• Where: OTM
• Authors: Thorsten Liebig, Felix Müller
• Keywords: DL Tableau Calculus, Internet Technology, OTM 2007, Reasoning, Tableau Algorithm