An Optimized KE-Tableau-Based System for Reasoning in the Description Logic D￡_D~(4,×)

摘要

We present a KE-tableau-based procedure for the main TBox and ABox reasoning tasks for the description logic DL<4LQS~(R,×)>(D), in short DL_D~(4,×). The logic DL_D~(4,×), representable in the decidable multi-sorted quantified set-theoretic fragment 4LQS～R, combines the high scalability and efficiency of rule languages such as the Semantic Web Rule Language (SWRL) with the expressivity of description logics. Our algorithm is based on a variant of the KE-tableau system for sets of universally quantified clauses, where the KE-elimination rule is generalized in such a way as to incorporate the γ-rule. The novel system, called KE~γ-tableau, turns out to improve both the system introduced in [3] and the standard first-order KE-tableaux [10]. Suitable benchmark test sets executed on С++ implementations of the three mentioned systems show that the performances of the KE~γ-tableau-based reasoner are often up to about 400% better than the ones of the other two systems. This a first step towards the construction of efficient reasoners for expressive OWL ontologies based on fragments of computable set theory.