Tableau Caching for Description Logics with Inverse and Transitive Roles

Abstract. Modern description logic (DL) reasoners are known to be less efficient for DLs with inverse roles. The current loss of performance is largely due to the missing applicability of some well-known optimization techniques, especially the one for caching the satisfiability status of modal successors. In this paper, we present a rule synthesis technique from which an estimation of the potential back-propagation of constraints can be made. This estimation can be applied to both the concept classifier and the satisfiability tester. This paper presents a tableau caching technique for SHI as a first step to improving the performance of tableau-based DL reasoners for logics offering the use of inverse roles. The proposed techniques underwent a first empirical evaluation with a prototype DL reasoner for SHI using a set of synthetically generated knowledge bases. The initial results indicate an significant improvement in runtime performance once caching is effectively enabled. 1 Motivatio...

• Type: Conference
• Year: 2006
• Where: DLOG
• Authors: Yu Ding, Volker Haarslev
• Keywords: Automated Reasoning, DL Reasoners, DL Systems, DLOG 2006, Inverse Roles